-lemma aaa_lifts: ∀G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → ∀b,f,L2. ⬇*[b, f] L2 ≡ L1 →
- ∀T2. ⬆*[f] T1 ≡ T2 → ⦃G, L2⦄ ⊢ T2 ⁝ A.
-@fqup_wf_ind_eq #G0 #L0 #T0 #IH #G #L1 * *
+(* Note: it should use drops_split_trans_pair2 *)
+lemma aaa_lifts: ∀G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → ∀b,f,L2. ⬇*[b, f] L2 ≘ L1 →
+ ∀T2. ⬆*[f] T1 ≘ T2 → ⦃G, L2⦄ ⊢ T2 ⁝ A.
+@(fqup_wf_ind_eq (Ⓣ)) #G0 #L0 #T0 #IH #G #L1 * *