Add inversion_wff

1 files changed, 10 insertions, 0 deletions

diff --git a/src/Reflection/WfInversion.v b/src/Reflection/WfInversion.v
index 9954d6f6f..e63cfc931 100644
--- a/src/Reflection/WfInversion.v
+++ b/src/Reflection/WfInversion.v
@@ -141,3 +141,13 @@ Section language.
     Qed.
   End with_var.
 End language.
+
+Ltac inversion_wff_step :=
+  match goal with
+  | [ H : wff _ ?x ?y |- _ ]
+    => first [ is_var x; fail 1
+             | is_var y; fail 1
+             | idtac ];
+       apply wff_encode in H; unfold wff_code in H; simpl in H
+  end.
+Ltac inversion_wff := repeat inversion_wff_step.