proposition: Lemma vars_equiv : forall x (t : term), List.In x (ATerm.vars t) <-> In x (vars t).
proof: Proof. intros x t0. pattern t0. apply term_ind with (Q := fun n (ts : terms n) => List.In x (ATerm.vars_vec ts) <-> In x (vars_vec ts)). intro. simpl. set_iff. tauto. intros. rewrite ATerm.vars_fun, vars_fun. hyp. simpl. set_iff. refl. intros. simpl. set_iff. rewrite in_app. tauto. Qed.
imports: CoLoR(LogicUtil ASubstitution FSetUtil NatUtil BoolUtil EqUtil ATrs ListUtil VecUtil) Coq(OrderedTypeEx)