proposition: Lemma map_remove_commute: forall {A B : Type} (eqa : Deq A) (eqb : Deq B) (f: A->B) (r: A) (lvi: list A) (fi : injective_fun f), map f (remove eqa r lvi) = remove eqb (f r) (map f lvi).
proof: Proof. intros. induction lvi; auto. simpl. symmetry. cases_if as Ha; cases_if as Hb; subst; sp. - apply fi in Ha. subst; sp. - simpl. f_equal; auto. Qed.
imports: UsefulTypes bin_rels Omega