proposition: Lemma subset_diff : forall A eq, forall l1 l2 l3 : list A, subset (diff eq l1 l2) l3 <=> subset l2 (l3 ++ l1).
proof: Proof. unfold subset; sp; split; sp. apply in_app_iff. assert (LIn x l1 + !LIn x l1) by (apply in_deq; auto); sp. left; apply_hyp; apply in_diff; sp. allrw in_diff; sp. apply_in_hyp p. allrw in_app_iff; sp. Qed.
imports: UsefulTypes bin_rels Omega