/3 width=9 by cpm_bind, lifts_bind, ex2_2_intro/
| #J #W1 #U1 #HG #HL #HT #i #K #V #HLK destruct
elim (IH G L W1 … HLK) [| // ] #W2 #V2 #HW12 #HVW2
/3 width=9 by cpm_bind, lifts_bind, ex2_2_intro/
| #J #W1 #U1 #HG #HL #HT #i #K #V #HLK destruct
elim (IH G L W1 … HLK) [| // ] #W2 #V2 #HW12 #HVW2