proposition: Lemma vars_eqns_combine : forall n (us vs : terms n), vars_eqns (combine (list_of_vec vs) (list_of_vec us)) [=] union (vars_vec vs) (vars_vec us).
proof: Proof. induction us; simpl; intros. VOtac. simpl. sym. apply union_empty_l. VSntac vs. clear H. set (x := Vhead vs). set (ts := Vtail vs). simpl. unfold vars_eqn. simpl. trans (union (union (vars x) (vars h)) (union (vars_vec ts) (vars_vec us))). apply union_m. refl. apply IHus. split; set_iff; tauto. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)