proposition: Lemma memberb_app : forall A eq x, forall l1 l2 : list A, memberb eq x (l1 ++ l2) = memberb eq x l1 || memberb eq x l2.
proof: Proof. induction l1; simpl; sp. destruct (eq a x); sp. Qed.
imports: UsefulTypes bin_rels Omega