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