proposition: Lemma diff_cons_r : forall A eq x, forall l1 l2 : list A, diff eq l1 (x :: l2) = if memberb eq x l1 then diff eq l1 l2 else x :: diff eq l1 l2.
proof: Proof. induction l1; simpl; sp. destruct (eq a x); subst; auto. Qed.
imports: UsefulTypes bin_rels Omega