matita/matita/contribs/lambdadelta/basic_2/etc/da/da_da.etc

   1 (* Advanced inversion lemmas ************************************************)
   2
   3 lemma sta_inv_refl_pos: ∀h,g,G,L,T,l.  ⦃G, L⦄ ⊢ T ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T •[h] T → ⊥.
   4 #h #g #G #L #T #l #H1T #HTT
   5 lapply (sta_da_conf … HTT … H1T) -HTT <minus_plus_m_m #H2T
   6 lapply (da_mono … H2T … H1T) -h -G -L -T #H
   7 elim (plus_xySz_x_false 0 l 0 ?) //
   8 qed-.