proposition: Lemma vars_eqns_app : forall l m, vars_eqns (l ++ m) [=] union (vars_eqns l) (vars_eqns m).
proof: Proof. induction l; simpl; intros. sym. apply union_empty_l. trans (union (vars_eqn a) (union (vars_eqns l) (vars_eqns m))). apply union_m. refl. apply IHl. sym. apply union_assoc. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)