-lemma lsubd_da_trans: ∀h,g,G,L2,T,l. ⦃G, L2⦄ ⊢ T ▪[h, g] l →
- ∀L1. G ⊢ L1 ⫃▪[h, g] L2 → ⦃G, L1⦄ ⊢ T ▪[h, g] l.
-#h #g #G #L2 #T #l #H elim H -G -L2 -T -l
+lemma lsubd_da_trans: ∀h,g,G,L2,T,d. ⦃G, L2⦄ ⊢ T ▪[h, g] d →
+ ∀L1. G ⊢ L1 ⫃▪[h, g] L2 → ⦃G, L1⦄ ⊢ T ▪[h, g] d.
+#h #g #G #L2 #T #d #H elim H -G -L2 -T -d