proposition: Lemma eq_gmaps : forall A B, forall l : list A, forall f g : (forall a : A, LIn a l -> B), (forall a (i : LIn a l), f a i = g a i) -> gmap l f = gmap l g.
proof: Proof. induction l; simpl; sp. generalize (H a (injL(eq_refl))); intro e. rewrite e. apply cons_eq; sp. Qed.
imports: UsefulTypes bin_rels Omega