X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Fdrops_lexs.ma;h=a192a206ecddcbabbb2093b499d68ac037090404;hb=f4787814123d74c9504e988137c2c13279838257;hp=d55d50dbbdf06e67958a5ec62c50028f9b0e220e;hpb=a78df6200d61b34a67cb1cba9edf984aae470530;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma
index d55d50dbb..a192a206e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma
@@ -152,3 +152,11 @@ elim (lexs_liftable_co_dedropable … H1RN H1RP H2RN H2RP … HLK1 … HK12 …
 #X #HX #HLK2 #H1L12 elim (lexs_inv_push1 … HX) -HX
 #L2 #V2 #H2L12 #HV12 #H destruct /2 width=6 by ex4_2_intro/
 qed-.
+
+lemma drops_atom2_lexs_conf: ∀RN,RP,b,f1,L1. ⬇*[b, f1] L1 ≡ ⋆ → 𝐔⦃f1⦄ →
+                             ∀f,L2. L1 ⦻*[RN, RP, f] L2 →
+                             ∀f2. f1 ~⊚ f2 ≡f → ⬇*[b, f1] L2 ≡ ⋆.
+#RN #RP #b #f1 #L1 #H1 #Hf1 #f #L2 #H2 #f2 #H3
+elim (lexs_co_dropable_sn … H1 … H2 … H3) // -H1 -H2 -H3 -Hf1
+#L #H #HL2 lapply (lexs_inv_atom1 … H) -H //
+qed-.