elim (lift_total T 0 (i+1))
/3 width=12 by lstas_ldef, cpcs_lift, ex2_intro/
| #V #l0 #_ #_ #_ #_ #_ #_ #_ #H destruct
]
| #G #L2 #K2 #X #Y #Y0 #U #i #l1 #HLK2 #HXY0 #_ #HYU #IHXY #l2 #Hl12 #Hl2 #L1 #HL12
elim (da_inv_lref … Hl2) -Hl2 * #K0 #V0 [| #l0 ] #HK0 #HV0 [| #H1 ]
elim (lift_total T 0 (i+1))
/3 width=12 by lstas_ldef, cpcs_lift, ex2_intro/
| #V #l0 #_ #_ #_ #_ #_ #_ #_ #H destruct
]
| #G #L2 #K2 #X #Y #Y0 #U #i #l1 #HLK2 #HXY0 #_ #HYU #IHXY #l2 #Hl12 #Hl2 #L1 #HL12
elim (da_inv_lref … Hl2) -Hl2 * #K0 #V0 [| #l0 ] #HK0 #HV0 [| #H1 ]