/2 width=3/ qed-.
fact snv_inv_cast_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀W,T. X = ⓝW.T →
/2 width=3/ qed-.
fact snv_inv_cast_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀W,T. X = ⓝW.T →
- ∃∃U,l. ⦃h, L⦄ ⊩ W :[g] & ⦃h, L⦄ ⊩ T :[g] &
+ ∃∃U,l. ⦃h, L⦄ ⊩ W :[g] & ⦃h, L⦄ ⊩ T :[g] &
⦃h, L⦄ ⊢ T •[g, l + 1] U & L ⊢ U ⬌* W.
#h #g #L #X * -L -X
[ #L #k #W #T #H destruct
⦃h, L⦄ ⊢ T •[g, l + 1] U & L ⊢ U ⬌* W.
#h #g #L #X * -L -X
[ #L #k #W #T #H destruct