proposition: Theorem assert_memberb : forall {T:Type} {eq : Deq T} (a:T) (l: list T), assert (memberb eq a l) <=> LIn a l.
proof: Proof. intros. induction l. simpl. try (unfold assert; repeat split; intros Hf; auto ; inversion Hf). simpl. destruct (eq a0 a) as [Heq | Hneq]. subst. unfold assert; repeat split; auto. repeat split; intros Hlr. right. apply IHl; auto. destruct Hlr as [Heq | Hin]. apply Hneq in Heq. contradiction. apply IHl; auto. Qed.
imports: UsefulTypes bin_rels Omega