proposition: Lemma cp_arr : forall P Q, cp P -> cp Q -> cp (arr P Q).
proof: Proof. intros P Q [p1 p2 p3 p4] [q1 q2 q3 q4]. constructor. apply cp_aeq_arr; fo. apply cp_sn_arr; fo. apply cp_red_arr; fo. apply cp_neutral_arr; fo. Qed.
imports: Coq(Morphisms Basics) CoLoR(RelUtil VecUtil VecOrd LogicUtil SN SetUtil)