fact: Fixpoint is_a_total_oc_ordering sigma c {struct c} := match c with | nil => true | x :: c' => let vx := Var x in let v_val := apply_subst sigma vx in if list_exists (fun z => var_in_term z v_val) c then false else is_a_total_oc_ordering sigma c' 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)