fact: Fixpoint Comb (l : list term) : term := match l with | nil => Term bot nil | t :: l => Term pi (t :: (Comb l) :: nil) end.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp graph_dp terminaison interp)