(* Basic properties *********************************************************)
+lemma drops_atom_F: ∀f. ⬇*[Ⓕ, f] ⋆ ≡ ⋆.
+#f @drops_atom #H destruct
+qed.
+
lemma drops_eq_repl_back: ∀b,L1,L2. eq_repl_back … (λf. ⬇*[b, f] L1 ≡ L2).
#b #L1 #L2 #f1 #H elim H -f1 -L1 -L2
[ /4 width=3 by drops_atom, isid_eq_repl_back/
| #f2 #I #L1 #L2 #V #_ #IHL #J #K #W #H elim (IHL … H) -IHL
/3 width=7 by after_next, ex3_2_intro, drops_drop/
| #f2 #I #L1 #L2 #V1 #V2 #HL #_ #_ #J #K #W #H destruct
- lapply (isid_after_dx 𝐈𝐝 … f2) /3 width=9 by after_push, ex3_2_intro, drops_drop/
+ lapply (after_isid_dx 𝐈𝐝 … f2) /3 width=9 by after_push, ex3_2_intro, drops_drop/
]
qed-.
(* 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.
[ #H elim (isid_inv_next … H) -H //
| /2 width=5 by ex2_3_intro/
]
-qed-.
+qed-.
+
+(* Properties with uniform relocations **************************************)
+
+lemma drops_uni_ex: ∀L,i. ⬇*[Ⓕ, 𝐔❴i❵] L ≡ ⋆ ∨ ∃∃I,K,V. ⬇*[i] L ≡ K.ⓑ{I}V.
+#L elim L -L /2 width=1 by or_introl/
+#L #I #V #IH * /4 width=4 by drops_refl, ex1_3_intro, or_intror/
+#i elim (IH i) -IH /3 width=1 by drops_drop, or_introl/
+* /4 width=4 by drops_drop, ex1_3_intro, or_intror/
+qed-.
(* Basic_2A1: removed theorems 12:
drops_inv_nil drops_inv_cons d1_liftable_liftables