proposition: Lemma cp_sn_arr : forall P Q, cp_aeq P -> cp_sn P -> cp_neutral P -> cp_sn Q -> cp_sn (arr P Q).
proof: Proof. intros P Q p1 p2 p4 q2 t ht. apply SN_st_app_l with (v:=Var(var_notin XSet.empty)). class. apply q2. apply ht. apply cp_var; hyp. Qed.
imports: Coq(Morphisms Basics) CoLoR(RelUtil VecUtil VecOrd LogicUtil SN SetUtil)