fact: Fixpoint Pi_red (t : term) : list term := match t with | Var _ => nil | Term f l => let Pi_red_list := (fix 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) in if F.Symb.eq_bool f pi then match l with | t1 :: t2 :: nil => t1 :: t2 :: map (fun l' => Term pi l') (Pi_red_list l) | _ =>map (fun l' => Term pi l') (Pi_red_list l) end else map (fun l' => Term f l') (Pi_red_list l) end.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)