proposition: Lemma cp_var_app_sn : forall P, cp_aeq P -> cp_neutral P -> forall x n (us : Tes n), Vforall (SN R_aeq) us -> P (apps (Var x) us).
proof: Proof. intros P p1 p4 x n us h. cut (SN (Vrel1 R_aeq) us). clear h. revert us. induction 1. rename x0 into us. apply p4. apply neutral_apps_var. intros v r. destruct (R_aeq_apps_neutral (neutral_var x) r). destruct H1 as [x' [h1 h2]]. apply not_R_aeq_var in h2. tauto. destruct H1 as [us' [h1 h2]]. rewrite h1. apply H0. hyp. apply Vforall_SN_rel1. hyp. Qed.
imports: Coq(Morphisms Basics) CoLoR(RelUtil VecUtil VecOrd LogicUtil SN SetUtil)