diff options
author | Jason Gross <jgross@mit.edu> | 2016-12-03 16:07:40 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2016-12-03 16:07:40 -0500 |
commit | c919ded4f0c43ddeebc3d414f86251018ffabb4f (patch) | |
tree | 0dc6f7ee0646f8e75374f11614e9ec30fac71345 /src/Reflection/WfInversion.v | |
parent | 156a62a1b542c9c2871d845a82bb44a3c7c39805 (diff) |
Add inversion_wff
Diffstat (limited to 'src/Reflection/WfInversion.v')
-rw-r--r-- | src/Reflection/WfInversion.v | 10 |
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. |