proposition: Lemma map_gmap_eq : forall {A B : Type} (l: list A) (f : forall a, LIn a l -> B) (g: A->B), (forall a (p: LIn a l), f a p = g a) -> map g l = gmap l f.
proof: Proof. induction l as [| a l Hind]; introv Heq;[reflexivity | ]. simpl. f_equal. rewrite Heq. reflexivity. apply Hind. intros. rewrite Heq; reflexivity. Qed.
imports: UsefulTypes bin_rels Omega