include "basic_2/reducibility/cfpr_cpr.ma".
-(* FOCALIZED PARALLEL REDUCTION ON CLOSURES *********************************)
+(* 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 *******************************************************)