+theorem drops_conf_div: ∀f1,L,K. ⬇*[Ⓣ,f1] L ≘ K → ∀f2. ⬇*[Ⓣ,f2] L ≘ K →
+ 𝐔⦃f1⦄ → 𝐔⦃f2⦄ → f1 ≡ f2.
+#f1 #L #K #H elim H -f1 -L -K
+[ #f1 #Hf1 #f2 #Hf2 elim (drops_inv_atom1 … Hf2) -Hf2
+ /3 width=1 by isid_inv_eq_repl/
+| #f1 #I #L #K #Hf1 #IH #f2 elim (pn_split f2) *
+ #g2 #H2 #Hf2 #HU1 #HU2 destruct
+ [ elim (drops_inv_skip1 … Hf2) -IH -HU1 -Hf2 #Y2 #X2 #HY2 #_ #H destruct
+ lapply (drops_fwd_isid … HY2 ?) -HY2 /2 width=3 by isuni_inv_push/ -HU2
+ #H destruct elim (drops_inv_x_bind_xy … Hf1)
+ | /4 width=5 by drops_inv_drop1, isuni_inv_next, eq_next/
+ ]
+| #f1 #I1 #I2 #L #K #Hf1 #_ #IH #f2 elim (pn_split f2) *
+ #g2 #H2 #Hf2 #HU1 #HU2 destruct
+ [ elim (drops_inv_skip1 … Hf2) -Hf2 #Y2 #X2 #HY2 #_ #H destruct -Hf1
+ /4 width=5 by isuni_fwd_push, eq_push/
+ | lapply (drops_inv_drop1 … Hf2) -Hf2 -IH -HU2 #Hg2
+ lapply (drops_fwd_isid … Hf1 ?) -Hf1 /2 width=3 by isuni_inv_push/ -HU1
+ #H destruct elim (drops_inv_x_bind_xy … Hg2)
+ ]
+]
+qed-.
+