proposition: Lemma forallb_forall : forall l, forallb l = true <-> (forall x, In x l -> f x = true).
proof: Proof. intro l; induction l as [|a l IHl]; simpl; [ tauto | split; intro H ]. + destruct (andb_prop _ _ H); intros a' [?|?]. - congruence. - apply IHl; assumption. + apply andb_true_intro; split. - apply H; left; reflexivity. - apply IHl; intros; apply H; right; assumption. Qed.
imports: PeanoNat