proposition: Lemma var_in_domain_of_subst : forall v sigma, VSet.mem v (domain_of_subst sigma) <-> (find X.eq_bool v sigma <> None).
proof: Proof. intros v sigma; induction sigma as [ | [x t] sigma]; simpl; split; intro H. contradiction. apply H; reflexivity. generalize (X.eq_bool_ok v x); case (X.eq_bool v x); [intro v_eq_x | intro v_diff_x]. discriminate. rewrite <- IHsigma. destruct (VSet.add_12 _ _ _ H) as [v_eq_x | v_in_dom]; [idtac | assumption]. absurd (v = x); trivial. revert H; generalize (X.eq_bool_ok v x); case (X.eq_bool v x); [intros v_eq_x _ | intros v_diff_x H]. subst x; apply VSet.add_1. apply VSet.add_2; rewrite IHsigma; assumption. Qed.
imports: Coq(Arith Wf_nat Wellfounded List Multiset Relations) CoLoR(closure decidable_set ordered_set more_list list_permut list_set list_sort dickson term_spec term)