Goal:
    A : Type  B : Type  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:
destruct m as [| m]

Goals:
    A : Type  B : Type  f : A -> option B  i : positive
  ============================
   (get i (map_filter f Empty) = option_map f (get i Empty))

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


DEBUG:Going to execute:
simpl
DEBUG LTAC Evaluated term: m