proposition: Lemma vars_eqns_subs : forall x v l, vars_eqns (map (eqn_sub (single x v)) l) [=] if mem x (vars_eqns l) then union (vars v) (remove x (vars_eqns l)) else vars_eqns l.
proof: Proof. induction l; simpl; intros. refl. mem. trans (union (if mem x (vars_eqn a) then union (vars v) (remove x (vars_eqn a)) else vars_eqn a) (if mem x (vars_eqns l) then union (vars v) (remove x (vars_eqns l)) else vars_eqns l)). apply union_m. apply vars_eqn_sub. exact IHl. case_eq (mem x (vars_eqn a)); case_eq (mem x (vars_eqns l)); intros H H0; bool. trans (union (vars v) (union (remove x (vars_eqn a)) (remove x (vars_eqns l)))). apply union_idem_3. apply union_m. refl. sym. apply remove_union. trans (union (vars v) (union (remove x (vars_eqn a)) (vars_eqns l))). apply union_assoc. apply union_m. refl. trans (union (remove x (vars_eqn a)) (remove x (vars_eqns l))). apply union_m. refl. sym. apply remove_equal. apply mem_4. hyp. sym. apply remove_union. trans (union (vars v) (union (vars_eqn a) (remove x (vars_eqns l)))). apply union_sym_2. apply union_m. refl. trans (union (remove x (vars_eqn a)) (remove x (vars_eqns l))). apply union_m. sym. apply remove_equal. apply mem_4. hyp. refl. sym. apply remove_union. refl. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)