X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fgrammar%2Flenv.ma;h=ff183d177d77db041663f15645ee2cda1a8c61e4;hb=c60524dec7ace912c416a90d6b926bee8553250b;hp=49d6cf5b83e309207cd7ea4201dc3e1a2d4b8b42;hpb=f10cfe417b6b8ec1c7ac85c6ecf5fb1b3fdf37db;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..ff183d177 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,6 @@ 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-.