X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Fdrops.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Fdrops.ma;h=9a4cfca83fa7b546da7072dcaa8d6a32d1e3637c;hb=926796df5884453d8f0cf9f294d7776d469ef45b;hp=8d22bcf00d89694df8aea6ff481ad5b43b944df1;hpb=e06774421eb3b8f4438a6876cc1ab4262ef16f6e;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma
index 8d22bcf00..9a4cfca83 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma
@@ -282,6 +282,18 @@ lemma drops_inv_TF: ∀f,I,L,K,V. ⬇*[Ⓕ, f] L ≡ K.ⓑ{I}V → 𝐔⦃f⦄ 
 
 (* Advanced inversion lemmas ************************************************)
 
+lemma drops_inv_atom2: ∀b,L,f. ⬇*[b,f] L ≡ ⋆ →
+                       ∃∃n,f1. ⬇*[b,𝐔❴n❵] L ≡ ⋆ & 𝐔❴n❵ ⊚ f1 ≡ f.
+#b #L elim L -L
+[ /3 width=4 by drops_atom, after_isid_sn, ex2_2_intro/
+| #L #I #V #IH #f #H elim (pn_split f) * #g #H0 destruct
+  [ elim (drops_inv_skip1 … H) -H #K #W #_ #_ #H destruct
+  | lapply (drops_inv_drop1 … H) -H #HL
+    elim (IH … HL) -IH -HL /3 width=8 by drops_drop, after_next, ex2_2_intro/
+  ]
+]
+qed-.
+
 (* Basic_2A1: includes: drop_inv_gen *)
 lemma drops_inv_gen: ∀b,f,I,L,K,V. ⬇*[b, f] L ≡ K.ⓑ{I}V → 𝐔⦃f⦄ →
                      ⬇*[Ⓣ, f] L ≡ K.ⓑ{I}V.