#g #Hg #H destruct /3 width=3 by drops_inv_drop1/
| #f1 #I #K1 #K #V1 #V #_ #HV1 #IH #b2 #f #L2 #HL2 #f2 #Hf elim (after_inv_pxx … Hf) -Hf [1,3: * |*:// ]
#g2 #g #Hf #H1 #H2 destruct
#g #Hg #H destruct /3 width=3 by drops_inv_drop1/
| #f1 #I #K1 #K #V1 #V #_ #HV1 #IH #b2 #f #L2 #HL2 #f2 #Hf elim (after_inv_pxx … Hf) -Hf [1,3: * |*:// ]
#g2 #g #Hf #H1 #H2 destruct
(* Basic_2A1: includes: drop_mono *)
lemma drops_mono: ∀b1,f,L,L1. ⬇*[b1, f] L ≡ L1 →
∀b2,L2. ⬇*[b2, f] L ≡ L2 → L1 = L2.
(* Basic_2A1: includes: drop_mono *)
lemma drops_mono: ∀b1,f,L,L1. ⬇*[b1, f] L ≡ L1 →
∀b2,L2. ⬇*[b2, f] L ≡ L2 → L1 = L2.
+
+lemma drops_inv_uni: ∀L,i. ⬇*[Ⓕ, 𝐔❴i❵] L ≡ ⋆ → ∀I,K,V. ⬇*[i] L ≡ K.ⓑ{I}V → ⊥.
+#L #i #H1 #I #K #V #H2
+lapply (drops_F … H2) -H2 #H2
+lapply (drops_mono … H2 … H1) -L -i #H destruct
+qed-.