proposition: Lemma sub_fun_sn : forall f ts x s, In x (vars (Fun f ts)) -> Vforall SNR (Vmap (sub s) ts) -> SNR (s x).
proof: Proof. intros. change (SNR (sub s (Var x))). rewrite vars_fun in H. ded (in_vars_vec_elim H). destruct H1 as [t]. destruct H1. ded (in_vars_subterm_eq H2). apply subterm_eq_sn with (t := sub s t). eapply Vforall_in with (n := arity f). apply H0. apply Vin_map_intro. hyp. apply subterm_eq_sub. hyp. Qed.
imports: CoLoR(ATrs SN LogicUtil VecUtil VecOrd NatUtil RelUtil ARelation Union ACap ACalls) Coq(List Sumbool)