proposition: Lemma vars_eqn_sub : forall x v e, vars_eqn (eqn_sub (single x v) e) [=] if mem x (vars_eqn e) then union (vars v) (remove x (vars_eqn e)) else vars_eqn e.
proof: Proof. intros. destruct e as [l r]. unfold vars_eqn, eqn_sub. simpl. trans (union (if mem x (vars l) then union (vars v) (remove x (vars l)) else vars l) (if mem x (vars r) then union (vars v) (remove x (vars r)) else vars r)). apply union_m; apply vars_single. mem. case_eq (mem x (vars l)); case_eq (mem x (vars r)); intros H H0; bool. trans (union (vars v) (union (remove x (vars l)) (remove x (vars r)))). apply union_idem_3. apply union_m. refl. sym. apply remove_union. trans (union (vars v) (union (remove x (vars l)) (vars r))). apply union_assoc. apply union_m. refl. trans (union (remove x (vars l)) (remove x (vars r))). apply union_m. refl. sym. apply remove_equal. apply mem_4. hyp. sym. apply remove_union. trans (union (vars v) (union (vars l) (remove x (vars r)))). apply union_sym_2. apply union_m. refl. trans (union (remove x (vars l)) (remove x (vars r))). 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)