-lemma snv_inv_cast: ∀h,g,L,W,T. ⦃h, L⦄ ⊩ ⓝW.T :[g] →
- ∃∃U,l. ⦃h, L⦄ ⊩ W :[g] & ⦃h, L⦄ ⊩ T :[g] &
- ⦃h, L⦄ ⊢ T •[g, l + 1] U & L ⊢ U ⬌* W.
-/2 width=3/ qed-.
+lemma snv_inv_appl: ∀h,o,G,L,V,T. ⦃G, L⦄ ⊢ ⓐV.T ¡[h, o] →
+ ∃∃a,W0,U0,d. ⦃G, L⦄ ⊢ V ¡[h, o] & ⦃G, L⦄ ⊢ T ¡[h, o] &
+ ⦃G, L⦄ ⊢ V •*➡*[h, o, 1] W0 & ⦃G, L⦄ ⊢ T •*➡*[h, o, d] ⓛ{a}W0.U0.
+/2 width=3 by snv_inv_appl_aux/ qed-.
+
+fact snv_inv_cast_aux: ∀h,o,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, o] → ∀U,T. X = ⓝU.T →
+ ∃∃U0. ⦃G, L⦄ ⊢ U ¡[h, o] & ⦃G, L⦄ ⊢ T ¡[h, o] &
+ ⦃G, L⦄ ⊢ U •*➡*[h, o, 0] U0 & ⦃G, L⦄ ⊢ T •*➡*[h, o, 1] U0.
+#h #o #G #L #X * -G -L -X
+[ #G #L #s #X1 #X2 #H destruct
+| #I #G #L #K #V #i #_ #_ #X1 #X2 #H destruct
+| #a #I #G #L #V #T #_ #_ #X1 #X2 #H destruct
+| #a #G #L #V #W0 #T #U0 #d #_ #_ #_ #_ #X1 #X2 #H destruct
+| #G #L #U #T #U0 #HV #HT #HU0 #HTU0 #X1 #X2 #H destruct /2 width=3 by ex4_intro/
+]
+qed-.
+
+lemma snv_inv_cast: ∀h,o,G,L,U,T. ⦃G, L⦄ ⊢ ⓝU.T ¡[h, o] →
+ ∃∃U0. ⦃G, L⦄ ⊢ U ¡[h, o] & ⦃G, L⦄ ⊢ T ¡[h, o] &
+ ⦃G, L⦄ ⊢ U •*➡*[h, o, 0] U0 & ⦃G, L⦄ ⊢ T •*➡*[h, o, 1] U0.
+/2 width=3 by snv_inv_cast_aux/ qed-.