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