fact: Fixpoint allb@{} (ls : list T) : bool := match ls with | nil => true | l :: ls => if p l then allb ls else false end.
imports: Coq.Lists.List ExtLib.Core.RelDec ExtLib.Structures.Monoid ExtLib.Structures.Reducible ExtLib.Tactics.Consider ExtLib.Tactics.Injection