1 (* Forward lemmas on stratified static type assignment for terms ************)
3 lemma aaa_fwd_ssta: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∃U. ⦃G, L⦄ ⊢ T •[h, g] U.
4 #h #G #L #T #A #H elim H -G -L -T -A
6 | * #G #L #K [ #V | #W ] #B #i #HLK #_ * [ #W | #V ] #HVW
7 elim (lift_total W 0 (i+1)) /3 width=7/
8 | #a #G #L #V #T #B #A #_ #_ #_ * /3 width=2/
9 | #a #G #L #V #T #B #A #_ #_ #_ * /3 width=2/
10 | #G #L #V #T #B #A #_ #_ #_ * /3 width=2/
11 | #G #L #W #T #A #_ #_ #_ * /3 width=2/