proposition: Lemma gmap2: forall (i: key)(m1:t A)(m2: t B), f None None = None -> find i (_map2 m1 m2) = f (find i m1) (find i m2).
proof: Proof. induction i; intros; destruct m1; destruct m2; simpl; auto; try apply xgmap2_r; try apply xgmap2_l; auto. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface