proposition: Lemma forallb_lforall f (fok : forall x, f x = true <-> P x) : forall l, forallb f l = true <-> lforall l.
proof: Proof. induction l; simpl. tauto. rewrite andb_eq, fok. intuition. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)