proposition: Lemma eq_maps : forall A B, forall f g : A -> B, forall l : list A, (forall x, LIn x l -> f x = g x) -> map f l = map g l.
proof: Proof. induction l; simpl; sp. assert (f a = g a). apply H; left; auto. rewrite H0. rewrite IHl; auto. Qed.
imports: UsefulTypes bin_rels Omega