X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fetc%2Flsx%2Flsx.etc;h=f09dc1da874da7a1eb8cb2d688b18167e716797b;hb=ec261374a2990bebeded039a64c0be0795ad9e93;hp=b5407abdf26155c986321c697494929cb1775229;hpb=6b35f96790b871aa06b22045b4e8e8dd7bba6590;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsx/lsx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsx/lsx.etc
index b5407abdf..f09dc1da8 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/lsx/lsx.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lsx/lsx.etc
@@ -6,7 +6,7 @@ lemma lsx_lreq_conf: ∀h,o,G,L1,T,l. G ⊢ ⬊*[h, o, T, l] L1 →
 #L0 #HL03 #HL10 #H elim (H T) -H /4 width=4 by/
 qed-.
 
-(* these two are better expressed with the binder \chi *)
+(* this is better expressed with the binder \chi *)
 
 lemma lsx_fwd_bind_dx: ∀h,o,a,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓑ{a,I}V.T, l] L →
                        G ⊢ ⬈*[h, o, T, ⫯l] L.ⓑ{I}V.
@@ -19,7 +19,3 @@ lemma lsx_fwd_bind_dx: ∀h,o,a,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓑ{a,I}V.T, l] L
 @(lleq_lreq_trans … (L2.ⓑ{I}V1))
 /2 width=2 by lleq_fwd_bind_dx, lreq_succ/
 qed-.
-
-lemma lsx_inv_bind: ∀h,o,a,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓑ{a, I}V.T, l] L →
-                    G ⊢ ⬈*[h, o, V, l] L ∧ G ⊢ ⬈*[h, o, T, ⫯l] L.ⓑ{I}V.
-/3 width=4 by lsx_fwd_bind_sn, lsx_fwd_bind_dx, conj/ qed-.