proposition: Lemma acc_inst_dom : forall c sigma, domain_of_subst sigma = domain_of_subst (acc_inst c sigma).
proof: Proof. intro c; induction c as [ | x l]; simpl; intros sigma; trivial. rewrite <- IHl. rewrite domain_of_subst_map_subst; reflexivity. 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)