1 (* Advanced properties ******************************************************)
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 ?) //