- degree-based equivalene for terms

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / etc_2A1 / fpn / fqu.etc

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_2A1/fpn/fqu.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_2A1/fpn/fqu.etc
new file mode 100644 (file)
index 0000000..1e4defb
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc_2A1/fpn/fqu.etc
@@ -0,0 +1,14 @@
+include "basic_2/grammar/bteq.ma".
+
+lemma fqu_fwd_bteq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+                    ⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄ → ⊥.
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+[ #I #G #L #V * #_ #H elim (plus_xSy_x_false … H)
+| #I #G #L #V #T * #_ #_ #H elim (discr_tpair_xy_x … H)
+| #a #I #G #L #V #T * #_ #_ #H elim (discr_tpair_xy_y … H)
+| #I #G #L #V #T * #_ #_ #H elim (discr_tpair_xy_y … H)
+| #G #L #K #T #U #e #HLK #_ * #_ #H
+  lapply (ldrop_fwd_length_lt4 … HLK ?) // >H -L #H
+  elim (lt_refl_false … H)
+]
+qed-.