proposition: Lemma diff_cons_r_ni : forall A eq x, forall l1 l2 : list A, !LIn x l2 -> diff eq (x :: l1) l2 = diff eq l1 l2.
proof: Proof. induction l1; simpl; sp. induction l2; allsimpl; allrw not_over_or; sp. destruct (eq x a); try subst; sp. allrw; sp. rw (remove_trivial A x); sp. Qed.
imports: UsefulTypes bin_rels Omega