lemma lsubr_cpm_trans: ∀n,h,G. lsub_trans … (cpm n h G) lsubr.
#n #h #G #L1 #T1 #T2 * /3 width=5 by lsubr_cpg_trans, ex2_intro/
qed-.
-
-(* Advanced properties ******************************************************)
-
-(* Basic_1: was by definition: pr2_free *)
-(* Basic_2A1: includes: tpr_cpr *)
-lemma tpm_cpm: ∀n,h,G,T1,T2. ⦃G, ⋆⦄ ⊢ T1 ➡[n, h] T2 → ∀L. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2.
-#n #h #G #T1 #T2 #HT12 #L lapply (lsubr_cpm_trans … HT12 L ?) //
-qed.