Preferentially invert wff with two constructors

1 files changed, 14 insertions, 0 deletions

diff --git a/src/Reflection/WfInversion.v b/src/Reflection/WfInversion.v
index e6c88a1ae..1f7046176 100644
--- a/src/Reflection/WfInversion.v
+++ b/src/Reflection/WfInversion.v
@@ -135,6 +135,17 @@ Section language.
   End with_var.
 End language.
 
+Ltac is_expr_constructor arg :=
+  lazymatch arg with
+  | Op _ _ => idtac
+  | TT => idtac
+  | Var _ => idtac
+  | LetIn _ _ => idtac
+  | Pair _ _ => idtac
+  | Abs _ => idtac
+  | Return _ => idtac
+  end.
+
 Ltac inversion_wff_step :=
   let postprocess H :=
       (cbv [wff_code] in H;
@@ -145,6 +156,9 @@ Ltac inversion_wff_step :=
            end) in
   match goal with
   | [ H : wff _ ?x ?y |- _ ]
+    => is_expr_constructor x; is_expr_constructor y;
+       apply wff_encode in H; postprocess H
+  | [ H : wff _ ?x ?y |- _ ]
     => first [ is_var x; is_var y; fail 1
              | idtac ];
        apply wff_encode in H; postprocess H