#h #o #T1 #T2 #H elim H -T1 -T2 [||| * ]
[ #s1 #s2 #d #Hs1 #Hs2 #f #X #H >(lifts_inv_sort1 … H) -H
/3 width=5 by lifts_sort, tdeq_sort, ex2_intro/
#h #o #T1 #T2 #H elim H -T1 -T2 [||| * ]
[ #s1 #s2 #d #Hs1 #Hs2 #f #X #H >(lifts_inv_sort1 … H) -H
/3 width=5 by lifts_sort, tdeq_sort, ex2_intro/