(* CONTEXT-FREE PARALLEL REDUCTION ON CLOSURES ******************************)
+(* Properties on context-sensitive parallel reduction for terms *************)
+
+lemma cpr_fpr: ∀L,T1,T2. L ⊢ T1 ➡ T2 → ⦃L, T1⦄ ➡ ⦃L, T2⦄.
+/2 width=4/ qed.
+
(* Advanced propertis *******************************************************)
lemma fpr_bind_sn: ∀L1,L2,V1,V2. ⦃L1, V1⦄ ➡ ⦃L2, V2⦄ → ∀T1,T2. T1 ➡ T2 →