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=ff183d177d77db041663f15645ee2cda1a8c61e4;hpb=c60524dec7ace912c416a90d6b926bee8553250b;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 ff183d177..80738ebbd 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma
@@ -66,3 +66,6 @@ lemma discr_lpair_x_xy: ∀I,V,L. L = L.ⓑ{I}V → ⊥.
   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-.