- ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l →
- ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, g] l.
-#h #g #G #L1 #T1 #HT1 #l #Hl #T2 #H
+ ∀d. ⦃G, L1⦄ ⊢ T1 ▪[h, g] d →
+ ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, g] d.
+#h #g #G #L1 #T1 #HT1 #d #Hd #T2 #H