proposition: Lemma solved_var_inc_occ_in_subst : forall x z x_val sigma, find X.eq_bool x sigma = Some x_val -> VSet.mem z (set_of_variables x_val) -> VSet.mem z (set_of_variables_in_range_of_subst sigma).
proof: Proof. intros x z x_val sigma; induction sigma as [ | [v t] sigma]. intro; discriminate. intros x_sigma z_in_x_val; simpl in x_sigma; revert x_sigma. generalize (X.eq_bool_ok x v); case (X.eq_bool x v); [intro v_eq_x; subst v | intro v_diff_x]. intro x_sigma; apply VSet.union_1; injection x_sigma; intros; subst; trivial. intros x_sigma; apply VSet.union_2; apply IHsigma; trivial. 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)