proposition: Lemma map_diff_commute: forall {A B : Type} (eqa : Deq A) (eqb : Deq B) (f: A->B) (lvr lvi: list A) (fi : injective_fun f), map f (diff eqa lvr lvi) = diff eqb (map f lvr) (map f lvi).
proof: Proof. induction lvr as [| ? lvr IHlvr]; intros; try(repeat (rewrite diff_nil)); auto;[]. simpl. rewrite IHlvr; auto. f_equal; auto. apply map_remove_commute; auto. Qed.
imports: UsefulTypes bin_rels Omega