elim (lt_or_eq_or_gt i j) #Hij
[ /3 width=4 by lifts_lref_ge_minus, cpr_refl, ex2_2_intro/
| elim (lifts_total V (𝐔❨↑i❩)) #U2 #HU2
elim (lt_or_eq_or_gt i j) #Hij
[ /3 width=4 by lifts_lref_ge_minus, cpr_refl, ex2_2_intro/
| elim (lifts_total V (𝐔❨↑i❩)) #U2 #HU2