-lemma drops_conf_div_bind: ∀f1,f2,I1,I2,L,K.
- ⇩*[Ⓣ,f1] L ≘ K.ⓘ[I1] → ⇩*[Ⓣ,f2] L ≘ K.ⓘ[I2] →
- 𝐔❪f1❫ → 𝐔❪f2❫ → f1 ≡ f2 ∧ I1 = I2.
+lemma drops_conf_div_bind_isuni:
+ ∀f1,f2,I1,I2,L,K.
+ ⇩*[Ⓣ,f1] L ≘ K.ⓘ[I1] → ⇩*[Ⓣ,f2] L ≘ K.ⓘ[I2] →
+ 𝐔❪f1❫ → 𝐔❪f2❫ → f1 ≡ f2 ∧ I1 = I2.