+(* Properties on parallel computation for terms *****************************)
+
+lemma cprs_scpds_div: ∀h,o,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡* T →
+ ∀d. ⦃G, L⦄ ⊢ T1 ▪[h, o] d →
+ ∀T2,d2. ⦃G, L⦄ ⊢ T2 •*➡*[h, o, d2] T →
+ ⦃G, L⦄⊢ T1 •*⬌*[h, o, 0, d2] T2.
+#h #o #G #L #T1 #T #HT1 #d #Hd elim (da_lstas … Hd 0)
+#X1 #HTX1 #_ elim (cprs_strip … HT1 X1) -HT1
+/3 width=5 by scpds_strap1, scpds_div, lstas_cpr, ex4_2_intro/
+qed.
+