Goal:
    A : Type  B : Type
  ============================
   (forall (f : A -> option B) (m : tree' A) (i : positive),
    get i (map_filter' f m) = option_map f (get' i m))


DEBUG:Going to execute:
induction m; simpl; intros; rewrite gNode