X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsubstitution%2Flleq_lleq.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsubstitution%2Flleq_lleq.ma;h=ca8035680133d2490a74e2bc9e159a0852e32154;hb=e4be4188d549da5fde54cdc37a6fb4eb2469c15b;hp=01e08e9f9124939a65113db0fd3a883a9017cf3f;hpb=5f1066ffb3c6ed53f9bf17ae2a81a9c9db32dba7;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma
index 01e08e9f9..ca8035680 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma
@@ -85,6 +85,14 @@ lemma lleq_inv_lref_ge_sn: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i →
 /3 width=4 by lleq_sym, ex2_2_intro/
 qed-.
 
+lemma lleq_inv_lref_ge: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i →
+                        ∀I1,I2,K1,K2,V.
+                        ⇩[i] L1 ≡ K1.ⓑ{I1}V → ⇩[i] L2 ≡ K2.ⓑ{I2}V → K1 ⋕[V, 0] K2.
+#L1 #L2 #d #i #HL12 #Hdi #I1 #I2 #K1 #K2 #V #HLK1 #HLK2
+elim (lleq_inv_lref_ge_sn … HL12 … HLK1) // -L1 -d
+#J #Y #HY lapply (ldrop_mono … HY … HLK2) -L2 -i #H destruct //
+qed-.
+
 (* Advanced properties ******************************************************)
 
 lemma lleq_dec: ∀T,L1,L2,d. Decidable (L1 ⋕[T, d] L2).