fact: Fixpoint acc_inst c sigma {struct c} := match c with | nil => sigma | x :: c' => let xxval := (x, apply_subst sigma (Var x)) in let xxval_subst := xxval :: nil in (acc_inst c' (map_subst (fun _ t => (apply_subst xxval_subst t)) sigma)) end.
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)