fact: Definition ddp_list is_def rule_list := fold_left (fun acc (rule : term*term) => (let (lhs,rhs) := rule in (ddp_rule is_def lhs rhs))++acc) rule_list (@nil (term*term)).
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)