advances on cofrees allows to prove one direction of

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / relocation / ldrop.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
index 0b1f18ba4946e79f6e545d99fd0bbd3e08f1638f..75016aa639b43f9c1e7f9d32efd0bbb559074d0f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
@@ -422,9 +422,9 @@ lemma ldrop_fwd_lw_lt: ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ L2 → 0 < e → ♯{
 ]
 qed-.
 
-lemma ldrop_fwd_rfw: â\88\80I,L,K,V,i. â\87©[i] L â\89¡ K.â\93\91{I}V â\86\92 â\99¯{K, V} < â\99¯{L, #i}.
+lemma ldrop_fwd_rfw: â\88\80I,L,K,V,i. â\87©[i] L â\89¡ K.â\93\91{I}V â\86\92 â\88\80T. â\99¯{K, V} < â\99¯{L, T}.
 #I #L #K #V #i #HLK lapply (ldrop_fwd_lw … HLK) -HLK
-normalize in ⊢ (%→?%%); /2 width=1 by le_S_S/
+normalize in ⊢ (%→?→?%%); /3 width=3 by le_to_lt_to_lt/
 qed-.
 
 (* Advanced inversion lemmas ************************************************)