X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fgrammar%2Flenv.ma;h=80738ebbde5c366fa3ec33662696af5898d44aa0;hb=ad3ca38634cfae29e8c26d0ab23cb466407eca5e;hp=49d6cf5b83e309207cd7ea4201dc3e1a2d4b8b42;hpb=67c5cf7ae14c745a94defbe645c5406ccbcf514d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma
index 49d6cf5b8..80738ebbd 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma
@@ -54,8 +54,8 @@ qed-.
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma destruct_lpair_lpair: ∀I1,I2,L1,L2,V1,V2. L1.ⓑ{I1}V1 = L2.ⓑ{I2}V2 →
-                            ∧∧L1 = L2 & I1 = I2 & V1 = V2.
+fact destruct_lpair_lpair_aux: ∀I1,I2,L1,L2,V1,V2. L1.ⓑ{I1}V1 = L2.ⓑ{I2}V2 →
+                               ∧∧L1 = L2 & I1 = I2 & V1 = V2.
 #I1 #I2 #L1 #L2 #V1 #V2 #H destruct /2 width=1 by and3_intro/
 qed-.
 
@@ -63,6 +63,9 @@ lemma discr_lpair_x_xy: ∀I,V,L. L = L.ⓑ{I}V → ⊥.
 #I #V #L elim L -L
 [ #H destruct
 | #L #J #W #IHL #H
-  elim (destruct_lpair_lpair … H) -H #H1 #H2 #H3 destruct /2 width=1 by/ (**) (* destruct lemma needed *)
+  elim (destruct_lpair_lpair_aux … H) -H #H1 #H2 #H3 destruct /2 width=1 by/ (**) (* destruct lemma needed *)
 ]
 qed-.
+
+lemma discr_lpair_xy_x: ∀I,V,L. L.ⓑ{I}V = L→ ⊥.
+/2 width=4 by discr_lpair_x_xy/ qed-.