Goal:
  
  A : Type
  B : Type
  f : A -> option B
  l : tree A
  o : option A
  r : tree A
  ============================
   (match Node l o r with
    | Empty => Empty
    | Nodes m' => map_filter' f m'
    end =
    Node match l with
         | Empty => Empty
         | Nodes m' => map_filter' f m'
         end (option_map f o)
      match r with
      | Empty => Empty
      | Nodes m' => map_filter' f m'
      end)


DEBUG:Going to execute:
destruct l, o, r
DEBUG LTAC Evaluated term: (map_filter'_opt f m)
DEBUG LTAC Evaluated term: (map_filter' f m)
DEBUG LTAC Evaluated term: gmap_filter'
DEBUG LTAC Evaluated term: map_filter'_opt
DEBUG LTAC Evaluated term: map_filter'
DEBUG LTAC Evaluated term: map_filter'
DEBUG LTAC Evaluated term: map_filter'

Goals:
    A : Type  B : Type  f : A -> option B  a : A
  ============================
   (match Node Empty (Some a) Empty with
    | Empty => Empty
    | Nodes m' => map_filter' f m'
    end = Node Empty (option_map f (Some a)) Empty)

    A : Type  B : Type  f : A -> option B  a : A  t0 : tree' A
  ============================
   (match Node Empty (Some a) (Nodes t0) with
    | Empty => Empty
    | Nodes m' => map_filter' f m'
    end = Node Empty (option_map f (Some a)) (map_filter' f t0))

    A : Type  B : Type  f : A -> option B
  ============================
   (match Node Empty None Empty with
    | Empty => Empty
    | Nodes m' => map_filter' f m'
    end = Node Empty (option_map f None) Empty)

    A : Type  B : Type  f : A -> option B  t0 : tree' A
  ============================
   (match Node Empty None (Nodes t0) with
    | Empty => Empty
    | Nodes m' => map_filter' f m'
    end = Node Empty (option_map f None) (map_filter' f t0))

    A : Type  B : Type  f : A -> option B  t0 : tree' A  a : A
  ============================
   (match Node (Nodes t0) (Some a) Empty with
    | Empty => Empty
    | Nodes m' => map_filter' f m'
    end = Node (map_filter' f t0) (option_map f (Some a)) Empty)

    A : Type  B : Type  f : A -> option B  t0 : tree' A  a : A  t1 : tree' A
  ============================
   (match Node (Nodes t0) (Some a) (Nodes t1) with
    | Empty => Empty
    | Nodes m' => map_filter' f m'
    end = Node (map_filter' f t0) (option_map f (Some a)) (map_filter' f t1))

    A : Type  B : Type  f : A -> option B  t0 : tree' A
  ============================
   (match Node (Nodes t0) None Empty with
    | Empty => Empty
    | Nodes m' => map_filter' f m'
    end = Node (map_filter' f t0) (option_map f None) Empty)

    A : Type  B : Type  f : A -> option B  t0 : tree' A  t1 : tree' A
  ============================
   (match Node (Nodes t0) None (Nodes t1) with
    | Empty => Empty
    | Nodes m' => map_filter' f m'
    end = Node (map_filter' f t0) (option_map f None) (map_filter' f t1))


DEBUG:Going to execute:
reflexivity
DEBUG LTAC Evaluated term: l
DEBUG LTAC Evaluated term: o
DEBUG LTAC Evaluated term: o
DEBUG LTAC Evaluated term: r
DEBUG LTAC Evaluated term: r
DEBUG LTAC Evaluated term: r
DEBUG LTAC Evaluated term: r

Goals:
    A : Type  B : Type  f : A -> option B  a : A
  ============================
   (match Node Empty (Some a) Empty with
    | Empty => Empty
    | Nodes m' => map_filter' f m'
    end = Node Empty (option_map f (Some a)) Empty)

    A : Type  B : Type  f : A -> option B  a : A  t0 : tree' A
  ============================
   (match Node Empty (Some a) (Nodes t0) with
    | Empty => Empty
    | Nodes m' => map_filter' f m'
    end = Node Empty (option_map f (Some a)) (map_filter' f t0))

    A : Type  B : Type  f : A -> option B
  ============================
   (match Node Empty None Empty with
    | Empty => Empty
    | Nodes m' => map_filter' f m'
    end = Node Empty (option_map f None) Empty)

    A : Type  B : Type  f : A -> option B  t0 : tree' A
  ============================
   (match Node Empty None (Nodes t0) with
    | Empty => Empty
    | Nodes m' => map_filter' f m'
    end = Node Empty (option_map f None) (map_filter' f t0))

    A : Type  B : Type  f : A -> option B  t0 : tree' A  a : A
  ============================
   (match Node (Nodes t0) (Some a) Empty with
    | Empty => Empty
    | Nodes m' => map_filter' f m'
    end = Node (map_filter' f t0) (option_map f (Some a)) Empty)

    A : Type  B : Type  f : A -> option B  t0 : tree' A  a : A  t1 : tree' A
  ============================
   (match Node (Nodes t0) (Some a) (Nodes t1) with
    | Empty => Empty
    | Nodes m' => map_filter' f m'
    end = Node (map_filter' f t0) (option_map f (Some a)) (map_filter' f t1))

    A : Type  B : Type  f : A -> option B  t0 : tree' A
  ============================
   (match Node (Nodes t0) None Empty with
    | Empty => Empty
    | Nodes m' => map_filter' f m'
    end = Node (map_filter' f t0) (option_map f None) Empty)

    A : Type  B : Type  f : A -> option B  t0 : tree' A  t1 : tree' A
  ============================
   (match Node (Nodes t0) None (Nodes t1) with
    | Empty => Empty
    | Nodes m' => map_filter' f m'
    end = Node (map_filter' f t0) (option_map f None) (map_filter' f t1))


DEBUG:Going to execute:
fun => <coq-core.plugins.ltac::reflexivity@0>