proposition: Lemma diff_app_r : forall T eq, forall l1 l2 l3 : list T, diff eq l1 (l2 ++ l3) = diff eq l1 l2 ++ diff eq l1 l3.
proof: Proof. induction l1; simpl; sp. rewrite remove_app. rewrite IHl1; auto. Qed.
imports: UsefulTypes bin_rels Omega