lemma snv_shnv_cast: ∀h,g,G,L,U,T. ⦃G, L⦄ ⊢ ⓝU.T ¡[h, g] → ⦃G, L⦄ ⊢ ⓝU.T ¡[h, g, 0].
#h #g #G #L #U #T #H elim (snv_inv_cast … H) -H
#U0 #HU #HT #HU0 #HTU0 @shnv_cast // -HU -HT
lemma snv_shnv_cast: ∀h,g,G,L,U,T. ⦃G, L⦄ ⊢ ⓝU.T ¡[h, g] → ⦃G, L⦄ ⊢ ⓝU.T ¡[h, g, 0].
#h #g #G #L #U #T #H elim (snv_inv_cast … H) -H
#U0 #HU #HT #HU0 #HTU0 @shnv_cast // -HU -HT