proposition: Lemma Forall_eq_forall_mem : forall P l, Forall P l = (forall x, mem x l -> P x).
proof: Proof. Proof using. extens. introv. induction l; iff I. { introv IN. inverts IN. } { auto. } { introv IN. rew_listx in IN. inverts I. destruct IN; subst*. } { constructors. { apply I. rew_listx*. } { apply~ IHl. introv IN. apply~ I. rew_listx*. } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)