proposition: Lemma cp_red_arr : forall P Q, cp_red Q -> cp_red (arr P Q).
proof: Proof. intros P Q q3 v v' vv' hv u hu. eapply q3. eapply mon_app_l. class. apply vv'. refl. apply hv. hyp. Qed.
imports: Coq(Morphisms Basics) CoLoR(RelUtil VecUtil VecOrd LogicUtil SN SetUtil)