#G0 #L0 #U0 #IH #G #L * *
[ #s #HG #HL #HT #i #I #K #V #_ destruct -IH
/2 width=4 by lifts_sort, ex2_2_intro/
| #j #HG #HL #HT #i #I #K #V #HLK destruct -IH
elim (lt_or_eq_or_gt i j) #Hij
[ /3 width=4 by lifts_lref_ge_minus, cpx_refl, ex2_2_intro/
#G0 #L0 #U0 #IH #G #L * *
[ #s #HG #HL #HT #i #I #K #V #_ destruct -IH
/2 width=4 by lifts_sort, ex2_2_intro/
| #j #HG #HL #HT #i #I #K #V #HLK destruct -IH
elim (lt_or_eq_or_gt i j) #Hij
[ /3 width=4 by lifts_lref_ge_minus, cpx_refl, ex2_2_intro/