proposition: Lemma cp_neutral_arr : forall P Q, cp_sn P -> cp_red P -> cp_aeq Q -> cp_neutral Q -> cp_neutral (arr P Q).
proof: Proof. intros P Q p2 p3 q1 q4 v nv hv u. revert u. cut (forall u, SN R_aeq u -> P u -> Q (App v u)). intros h u hu. apply h. apply p2. hyp. hyp. induction 1. rename x into u. intro hu. apply q4. apply neutral_app. hyp. intros w r. destruct (R_aeq_app_neutral nv r). destruct H1 as [v' [h1 h2]]. rewrite h1. apply hv; hyp. destruct H1 as [u' [h1 h2]]. rewrite h1. apply H0. hyp. eapply p3. apply h2. hyp. Qed.
imports: Coq(Morphisms Basics) CoLoR(RelUtil VecUtil VecOrd LogicUtil SN SetUtil)