fact: Fixpoint intersperse (a : M.term) (ls : list (list M.term)) : list M.term := match ls with | l :: nil => l | l :: tl => l ++ a :: intersperse a tl | _ => nil end.
imports: Coq(Setoid List Relations Wellfounded PeanoNat) CoLoR(weaved_relation list_permut terminaison)