| ∃∃K1,V. K1 ⫃ K2 & L1 = K1.ⓓⓝW.V & I = Abst.
#I #L1 #K2 #W #H elim (lsubr_inv_bind2 … H) -H *
[ /3 width=3 by ex2_intro, or_introl/
| #K1 #X #V #HK12 #H1 #H2 destruct /3 width=4 by ex3_2_intro, or_intror/
| ∃∃K1,V. K1 ⫃ K2 & L1 = K1.ⓓⓝW.V & I = Abst.
#I #L1 #K2 #W #H elim (lsubr_inv_bind2 … H) -H *
[ /3 width=3 by ex2_intro, or_introl/
| #K1 #X #V #HK12 #H1 #H2 destruct /3 width=4 by ex3_2_intro, or_intror/