matita/matita/contribs/lambdadelta/basic_2/etc/cpm_lsubr.etc

   1 (* Advanced properties ******************************************************)
   2
   3 (* Basic_1: was by definition: pr2_free *)
   4 (* Basic_2A1: includes: tpr_cpr *)
   5 lemma tpm_cpm: ∀n,h,G,T1,T2. ⦃G, ⋆⦄ ⊢ T1 ➡[n, h] T2 → ∀L. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2.
   6 #n #h #G #T1 #T2 #HT12 #L lapply (lsubr_cpm_trans … HT12 L ?) //
   7 qed.