-lemma da_inv_lift: ∀h,g,G,L2,T2,l. ⦃G, L2⦄ ⊢ T2 ▪[h, g] l →
- ∀L1,s,d,e. ⬇[s, d, e] L2 ≡ L1 → ∀T1. ⬆[d, e] T1 ≡ T2 →
- ⦃G, L1⦄ ⊢ T1 ▪[h, g] l.
-#h #g #G #L2 #T2 #l #H elim H -G -L2 -T2 -l
-[ #G #L2 #k #l #Hkl #L1 #s #d #e #_ #X #H
+lemma da_inv_lift: ∀h,g,G,L2,T2,d. ⦃G, L2⦄ ⊢ T2 ▪[h, g] d →
+ ∀L1,s,l,m. ⬇[s, l, m] L2 ≡ L1 → ∀T1. ⬆[l, m] T1 ≡ T2 →
+ ⦃G, L1⦄ ⊢ T1 ▪[h, g] d.
+#h #g #G #L2 #T2 #d #H elim H -G -L2 -T2 -d
+[ #G #L2 #k #d #Hkd #L1 #s #l #m #_ #X #H