| #g #Hg #HLK1 #H destruct -HL12
elim (IH … Hg HLK1) -L1 -Hg /3 width=3 by drops_drop, ex2_intro/
]
| #g #Hg #HLK1 #H destruct -HL12
elim (IH … Hg HLK1) -L1 -Hg /3 width=3 by drops_drop, ex2_intro/
]
elim (drops_inv_bind1_isuni … Hf H) -Hf -H *
[ #Hf #H destruct -IH
/3 width=3 by drops_refl, lsubv_beta, ex2_intro/
elim (drops_inv_bind1_isuni … Hf H) -Hf -H *
[ #Hf #H destruct -IH
/3 width=3 by drops_refl, lsubv_beta, ex2_intro/
| #g #Hg #HLK2 #H destruct -HL12
elim (IH … Hg HLK2) -L2 -Hg /3 width=3 by drops_drop, ex2_intro/
]
| #g #Hg #HLK2 #H destruct -HL12
elim (IH … Hg HLK2) -L2 -Hg /3 width=3 by drops_drop, ex2_intro/
]
elim (drops_inv_bind1_isuni … Hf H) -Hf -H *
[ #Hf #H destruct -IH
/3 width=3 by drops_refl, lsubv_beta, ex2_intro/
elim (drops_inv_bind1_isuni … Hf H) -Hf -H *
[ #Hf #H destruct -IH
/3 width=3 by drops_refl, lsubv_beta, ex2_intro/