proposition: Lemma Forall_eq_count_eq_length : forall P l, Forall P l = (count P l = length l).
proof: Proof. Proof using. intros. induction l; rew_listx. { extens*. } { rewrite IHl. extens. iff (M1&M2) M; case_if. { math. } { split~. math. } { false. forwards~: count_le_length P l. math. } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)