+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-.