matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_length.ma

   1 (* Basic forward lemmas *****************************************************)
   2
   3 (* Forward lemmas with length for local environments ************************)
   4
   5 (* Basic_2A1: was just: lpxs_fwd_length *)
   6 lemma lfpxs_fwd_length: ∀h,o,G,L1,L2. ⦃G, L1⦄ ⊢ ⬈*[h, o] L2 → |L1| = |L2|.
   7 /2 width=2 by TC_lpx_sn_fwd_length/ qed-.