X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fgrammar%2Flsubs.ma;h=cf90a6134590c41c8ffc50b511cf5123e4fa3e49;hb=d38087520d6ce1d696b28da40f3811291fc8a311;hp=83169d811cae425dadcaa7c0bf01d9e5d733d42e;hpb=016603891d57b4c6b41da6a398bf8ae466019f9e;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma
index 83169d811..cf90a6134 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma
@@ -43,8 +43,8 @@ lemma TC_lsubs_conf: ∀S,R. lsubs_conf S R → lsubs_conf S (λL. (TC … (R L)
 ]
 qed.
 
-lemma lsubs_eq: ∀L1,L2,e. L1 [0, e] ≼ L2 → ∀I,V.
-                L1. 𝕓{I} V [0, e + 1] ≼ L2.𝕓{I} V.
+lemma lsubs_bind_eq: ∀L1,L2,e. L1 [0, e] ≼ L2 → ∀I,V.
+                     L1. 𝕓{I} V [0, e + 1] ≼ L2.𝕓{I} V.
 #L1 #L2 #e #HL12 #I #V elim I -I /2/
 qed.
 
@@ -78,7 +78,7 @@ fact lsubs_fwd_length_full1_aux: ∀L1,L2,d,e. L1 [d, e] ≼ L2 →
 qed.
 
 lemma lsubs_fwd_length_full1: ∀L1,L2. L1 [0, |L1|] ≼ L2 → |L1| ≤ |L2|.
-/2 width=5/ qed.
+/2 width=5/ qed-.
 
 fact lsubs_fwd_length_full2_aux: ∀L1,L2,d,e. L1 [d, e] ≼ L2 →
                                  d = 0 → e = |L2| → |L2| ≤ |L1|.
@@ -93,4 +93,4 @@ fact lsubs_fwd_length_full2_aux: ∀L1,L2,d,e. L1 [d, e] ≼ L2 →
 qed.
 
 lemma lsubs_fwd_length_full2: ∀L1,L2. L1 [0, |L2|] ≼ L2 → |L2| ≤ |L1|.
-/2 width=5/ qed.
+/2 width=5/ qed-.