fact: Fixpoint well_formed_cf (t:term) : Prop := match t with | Var _ => True | Term f l => let wf_cf_list := (fix wf_cf_list (l:list term) : Prop := match l with | nil => True | h :: tl => well_formed_cf h /\ wf_cf_list tl end) in wf_cf_list l /\ (match arity f with | Free n => length l = n | C => length l = 2 /\ is_sorted l | AC => length l >= 2 /\ is_sorted l /\ (forall s, In s l -> match s with | Var _ => True | Term g _ => f<>g end) end) end.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)