matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta_aaa.etc

   1 (* Forward lemmas on stratified static type assignment for terms ************)
   2
   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
   5 [ /2 width=2/
   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/
  12 ]
  13 qed-.