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