proposition: Lemma domain_of_subst_map_subst : forall sigma f, domain_of_subst (map_subst f sigma) = domain_of_subst sigma.
proof: Proof. intros sigma f; induction sigma as [ | [x t] sigma]; simpl; trivial; rewrite 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)