-lemma snv_fwd_ssta: ∀h,g,L,T. ⦃h, L⦄ ⊢ T ¡[g] → ∃∃l,U. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄.
-#h #g #L #T #H elim H -L -T
-[ #L #k elim (deg_total h g k) /3 width=3/
-| * #L #K #V #i #HLK #_ * #l0 #W #HVW
- [ elim (lift_total W 0 (i+1)) /3 width=8/
- | elim (lift_total V 0 (i+1)) /3 width=8/
- ]
-| #a #I #L #V #T #_ #_ #_ * /3 width=3/
-| #a #L #V #W #W1 #T0 #T1 #l #_ #_ #_ #_ #_ #_ * /3 width=3/
-| #L #W #T #U #l #_ #_ #HTU #_ #_ #_ /3 width=3/ (**) (* auto fails without the last #_ *)
+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/