proposition: Lemma in_diff : forall T, forall l1 l2 : list T, forall x eq, LIn x (diff eq l1 l2) <=> (LIn x l2 # (! LIn x l1)).
proof: Proof. induction l1; simpl; sp. split; sp. introv. auto. trw IHl1; trw in_remove; split; sp; auto. Qed.
imports: UsefulTypes bin_rels Omega