fact: Fixpoint Pi_red_list (l : list term) {struct l} : list (list term) := match l with | nil => nil | t :: lt => (map (fun t' => t' :: lt) (Pi_red t)) ++ (map (fun l' => t :: l') (Pi_red_list lt)) end.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)