X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsyntax%2Ftdeq.ma;h=d431b7677a55bd28dc55f1e47578c4c7d06cbcd9;hp=516c42904f65a58c53842bcc24c72fcac8ad8790;hb=4738096e93f997fb36d35dd723b87682a2f6de90;hpb=a5c71699f1d0cf63a769c71dd8b8cd5dfff1933d

diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma
index 516c42904..d431b7677 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma
@@ -101,6 +101,13 @@ lemma tdeq_inv_pair: ∀h,o,I1,I2,V1,V2,T1,T2. ②{I1}V1.T1 ≛[h, o] ②{I2}V2.
 #V0 #T0 #HV #HT #H destruct /2 width=1 by and3_intro/
 qed-.
 
+lemma tdeq_inv_pair_xy_x: ∀h,o,I,V,T. ②{I}V.T ≛[h, o] V → ⊥.
+#h #o #I #V elim V -V
+[ #J #T #H elim (tdeq_inv_pair1 … H) -H #X #Y #_ #_ #H destruct
+| #J #X #Y #IHX #_ #T #H elim (tdeq_inv_pair … H) -H #H #HY #_ destruct /2 width=2 by/
+]
+qed-.
+
 lemma tdeq_inv_pair_xy_y: ∀h,o,I,T,V. ②{I}V.T ≛[h, o] T → ⊥.
 #h #o #I #T elim T -T
 [ #J #V #H elim (tdeq_inv_pair1 … H) -H #X #Y #_ #_ #H destruct