proposition: Lemma in_app_deq : forall A l1 l2 (a : A) (deq : Deq A), LIn a (l1 ++ l2) -> (LIn a l1 + LIn a l2).
proof: Proof. introv deq i. rw <- (@assert_memberb A deq) in i. rw memberb_app in i. apply assert_orb in i; sp; allrw (@assert_memberb A deq); sp. Qed.
imports: UsefulTypes bin_rels Omega