-
-(* Basic forward lemmas *****************************************************)
-
-lemma snv_fwd_ssta: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ∃∃l,U. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄.
-#h #g #G #L #T #H elim H -G -L -T
-[ #G #L #k elim (deg_total h g k) /3 width=3/
-| * #G #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 #G #L #V #T #_ #_ #_ * /3 width=3/
-| #a #G #L #V #W #W1 #T0 #T1 #l #_ #_ #_ #_ #_ #_ * /3 width=3/
-| #G #L #W #T #U #l #_ #_ #HTU #_ #_ #_ /3 width=3/ (**) (* auto fails without the last #_ *)
-]
-qed-.