lemma teqo_lifts_sn: liftable2_sn teqo.
#T1 #T2 #H elim H -T1 -T2 [||| * ]
-[ #s1 #s2 #f #X #H
+[ #s1 #s2 #f #X #H
>(lifts_inv_sort1 … H) -H
/2 width=3 by teqo_sort, ex2_intro/
| #i #f #X #H
| #j #f #X1 #H1 #X2 #H2
elim (lifts_inv_lref2 … H1) -H1 #i1 #Hj1 #H destruct
elim (lifts_inv_lref2 … H2) -H2 #i2 #Hj2 #H destruct
- <(at_inj … Hj2 … Hj1) -j -f -i1
+ <(pr_pat_inj … Hj2 … Hj1) -j -f -i1
/1 width=1 by teqo_lref/
| #l #f #X1 #H1 #X2 #H2
>(lifts_inv_gref2 … H1) -H1 >(lifts_inv_gref2 … H2) -H2