proposition: Lemma gmap_length : forall (A B : Type) (l : list A) (f:(forall a : A, LIn a l -> B)), length (gmap l f)= length l.
proof: Proof. induction l; auto. intros. simpl. f_equal. rewrite IHl; auto. Qed.
imports: UsefulTypes bin_rels Omega