-| #J #L1 #L2 #V #HL12 #IH #b #f #I #K2 #W #Hf #H
- elim (drops_inv_pair1_isuni … Hf H) -Hf -H *
- [ #Hf #H destruct -IH
- /4 width=4 by drops_refl, ex2_intro, or_introl/
- | #g #Hg #HLK2 #H destruct -HL12
- elim (IH … Hg HLK2) -IH -Hg -HLK2 *
- /4 width=4 by drops_drop, ex3_2_intro, ex2_intro, or_introl, or_intror/
- ]
-| #L1 #L2 #V1 #V2 #HL12 #IH #b #f #I #K2 #W #Hf #H
- elim (drops_inv_pair1_isuni … Hf H) -Hf -H *
- [ #Hf #H destruct -IH
- /4 width=4 by drops_refl, ex3_2_intro, or_intror/
- | #g #Hg #HLK2 #H destruct -HL12
- elim (IH … Hg HLK2) -IH -Hg -HLK2 *
- /4 width=4 by drops_drop, ex3_2_intro, ex2_intro, or_introl, or_intror/
- ]
+| #J #L1 #L2 | #L1 #L2 #V #W | #I1 #I2 #L1 #L2 #V1
+]
+#HL12 #IH #b #f #I #K2 #Hf #H
+elim (drops_inv_bind1_isuni … Hf H) -Hf -H *
+[1,3,5: #Hf #H destruct -IH
+ /4 width=6 by drops_refl, or3_intro0, or3_intro1, or3_intro2, ex3_4_intro, ex3_3_intro, ex2_intro/
+|2,4,6: #g #Hg #HLK2 #H destruct -HL12
+ elim (IH … Hg HLK2) -IH -Hg -HLK2 *
+ /4 width=6 by drops_drop, or3_intro0, or3_intro1, or3_intro2, ex3_4_intro, ex3_3_intro, ex2_intro/