-fact snv_inv_appl_aux: ∀h,g,L,X. ⦃h, L⦄ ⊢ X ¡[g] → ∀V,T. X = ⓐV.T →
- ∃∃a,W,W0,U,l. ⦃h, L⦄ ⊢ V ¡[g] & ⦃h, L⦄ ⊢ T ¡[g] &
- ⦃h, L⦄ ⊢ V •[g] ⦃l+1, W⦄ & L ⊢ W ➡* W0 &
- ⦃h, L⦄ ⊢ T •*➡*[g] ⓛ{a}W0.U.
+fact snv_inv_appl_aux: ∀h,g,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀V,T. X = ⓐV.T →
+ ∃∃a,W,W0,U,l. ⦃G, L⦄ ⊢ V ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g] &
+ ⦃G, L⦄ ⊢ V •[h, g] ⦃l+1, W⦄ & ⦃G, L⦄ ⊢ W ➡* W0 &
+ ⦃G, L⦄ ⊢ T •*➡*[h, g] ⓛ{a}W0.U.