proposition: Lemma xgmap2_r : forall (i : key) (m : t B), f None None = None -> find i (xmap2_r m) = f None (find i m).
proof: Proof. induction i; intros; destruct m; simpl; auto. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface