-(* 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.
+lemma cpm_bind_unit (h) (n) (G): ∀L,V1,V2. ❪G,L❫ ⊢ V1 ➡[h,0] V2 →
+ ∀J,T1,T2. ❪G,L.ⓤ[J]❫ ⊢ T1 ➡[h,n] T2 →
+ ∀p,I. ❪G,L❫ ⊢ ⓑ[p,I]V1.T1 ➡[h,n] ⓑ[p,I]V2.T2.
+/4 width=4 by lsubr_cpm_trans, cpm_bind, lsubr_unit/ qed.