proposition: Lemma eq_gmapds : 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) -> gmapd l f = gmapd l g.
proof: Proof. intros. repeat (rw <- gmap_eq_d). apply eq_gmaps; sp. Qed.
imports: UsefulTypes bin_rels Omega