-(* Basic_2A1: includes: cprs_cpxs *)
-lemma cpms_fwd_cpxs (n) (h): â\88\80G,L,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡*[n, h] T2 â\86\92 â¦\83G, Lâ¦\84 ⊢ T1 ⬈*[h] T2.
+(* Basic_2A1: includes: scpds_fwd_cpxs cprs_cpxs *)
+lemma cpms_fwd_cpxs (n) (h): â\88\80G,L,T1,T2. â\9dªG,Lâ\9d« â\8a¢ T1 â\9e¡*[n,h] T2 â\86\92 â\9dªG,Lâ\9d« ⊢ T1 ⬈*[h] T2.