-| lsubsv_beta: ∀L1,L2,W,V,l1. ⦃G, L1⦄ ⊢ ⓝW.V ¡[h, g, l1] → ⦃G, L2⦄ ⊢ W ¡[h, g] →
- ⦃G, L1⦄ ⊢ V ▪[h, g] l1+1 → ⦃G, L2⦄ ⊢ W ▪[h, g] l1 →
+| lsubsv_beta: ∀L1,L2,W,V,d1. ⦃G, L1⦄ ⊢ ⓝW.V ¡[h, g, d1] → ⦃G, L2⦄ ⊢ W ¡[h, g] →
+ ⦃G, L1⦄ ⊢ V ▪[h, g] d1+1 → ⦃G, L2⦄ ⊢ W ▪[h, g] d1 →