Goal:
  
  A : Type
  B : Type
  C : Type
  f : option A -> option B -> option C
  f_None_None : f None None = None
  m1_1 : tree A
  o : option A
  m1_2 : tree A
  H : not_trivially_empty m1_1 o m1_2
  IHm1_1 : forall (m2 : tree B) (i : positive),
           get i
             (tree_rec (map_filter (fun b : B => f None (Some b)))
                (fun (l1 : tree A) (lrec : tree B -> tree C) 
                   (o1 : option A) (r1 : tree A) (rrec : tree B -> tree C) =>
                 tree_case
                   (map_filter (fun a : A => f (Some a) None) (Node l1 o1 r1))
                   (fun (l2 : tree B) (o2 : option B) (r2 : tree B) =>
                    Node (lrec l2) (f o1 o2) (rrec r2))) m1_1 m2) =
           f (get i m1_1) (get i m2)
  IHm1_2 : forall (m2 : tree B) (i : positive),
           get i
             (tree_rec (map_filter (fun b : B => f None (Some b)))
                (fun (l1 : tree A) (lrec : tree B -> tree C) 
                   (o1 : option A) (r1 : tree A) (rrec : tree B -> tree C) =>
                 tree_case
                   (map_filter (fun a : A => f (Some a) None) (Node l1 o1 r1))
                   (fun (l2 : tree B) (o2 : option B) (r2 : tree B) =>
                    Node (lrec l2) (f o1 o2) (rrec r2))) m1_2 m2) =
           f (get i m1_2) (get i m2)
  i : positive
  m2_1 : tree B
  o0 : option B
  m2_2 : tree B
  H0 : not_trivially_empty m2_1 o0 m2_2
  IHm2_1 : get i
             (tree_case
                (map_filter (fun a : A => f (Some a) None) (Node m1_1 o m1_2))
                (fun (l2 : tree B) (o2 : option B) (r2 : tree B) =>
                 Node
                   (tree_rec (map_filter (fun b : B => f None (Some b)))
                      (fun (l1 : tree A) (lrec : tree B -> tree C)
                         (o1 : option A) (r1 : tree A)
                         (rrec : tree B -> tree C) =>
                       tree_case
                         (map_filter (fun a : A => f (Some a) None)
                            (Node l1 o1 r1))
                         (fun (l3 : tree B) (o3 : option B) (r3 : tree B) =>
                          Node (lrec l3) (f o1 o3) (rrec r3))) m1_1 l2)
                   (f o o2)
                   (tree_rec (map_filter (fun b : B => f None (Some b)))
                      (fun (l1 : tree A) (lrec : tree B -> tree C)
                         (o1 : option A) (r1 : tree A)
                         (rrec : tree B -> tree C) =>
                       tree_case
                         (map_filter (fun a : A => f (Some a) None)
                            (Node l1 o1 r1))
                         (fun (l3 : tree B) (o3 : option B) (r3 : tree B) =>
                          Node (lrec l3) (f o1 o3) (rrec r3))) m1_2 r2)) m2_1) =
           f (get i (Node m1_1 o m1_2)) (get i m2_1)
  IHm2_2 : get i
             (tree_case
                (map_filter (fun a : A => f (Some a) None) (Node m1_1 o m1_2))
                (fun (l2 : tree B) (o2 : option B) (r2 : tree B) =>
                 Node
                   (tree_rec (map_filter (fun b : B => f None (Some b)))
                      (fun (l1 : tree A) (lrec : tree B -> tree C)
                         (o1 : option A) (r1 : tree A)
                         (rrec : tree B -> tree C) =>
                       tree_case
                         (map_filter (fun a : A => f (Some a) None)
                            (Node l1 o1 r1))
                         (fun (l3 : tree B) (o3 : option B) (r3 : tree B) =>
                          Node (lrec l3) (f o1 o3) (rrec r3))) m1_1 l2)
                   (f o o2)
                   (tree_rec (map_filter (fun b : B => f None (Some b)))
                      (fun (l1 : tree A) (lrec : tree B -> tree C)
                         (o1 : option A) (r1 : tree A)
                         (rrec : tree B -> tree C) =>
                       tree_case
                         (map_filter (fun a : A => f (Some a) None)
                            (Node l1 o1 r1))
                         (fun (l3 : tree B) (o3 : option B) (r3 : tree B) =>
                          Node (lrec l3) (f o1 o3) (rrec r3))) m1_2 r2)) m2_2) =
           f (get i (Node m1_1 o m1_2)) (get i m2_2)
  ============================
   (match i with
    | xI j =>
        get j
          (tree_rec (map_filter (fun b : B => f None (Some b)))
             (fun (l1 : tree A) (lrec : tree B -> tree C) 
                (o1 : option A) (r1 : tree A) (rrec : tree B -> tree C) =>
              tree_case
                (map_filter (fun a : A => f (Some a) None) (Node l1 o1 r1))
                (fun (l2 : tree B) (o2 : option B) (r2 : tree B) =>
                 Node (lrec l2) (f o1 o2) (rrec r2))) m1_2 m2_2)
    | xO j =>
        get j
          (tree_rec (map_filter (fun b : B => f None (Some b)))
             (fun (l1 : tree A) (lrec : tree B -> tree C) 
                (o1 : option A) (r1 : tree A) (rrec : tree B -> tree C) =>
              tree_case
                (map_filter (fun a : A => f (Some a) None) (Node l1 o1 r1))
                (fun (l2 : tree B) (o2 : option B) (r2 : tree B) =>
                 Node (lrec l2) (f o1 o2) (rrec r2))) m1_1 m2_1)
    | xH => f o o0
    end =
    f match i with
      | xI j => get j m1_2
      | xO j => get j m1_1
      | xH => o
      end
      match i with
      | xI j => get j m2_2
      | xO j => get j m2_1
      | xH => o0
      end)


DEBUG:Going to execute:
destruct i
DEBUG LTAC Evaluated term: unroll_tree_case
DEBUG LTAC Evaluated term: gNode
DEBUG LTAC Evaluated term: gNode
DEBUG LTAC Evaluated term: gNode
DEBUG LTAC Evaluated term: gNode
DEBUG LTAC Evaluated term: gNode

Goals:
  
  A : Type
  B : Type
  C : Type
  f : option A -> option B -> option C
  f_None_None : f None None = None
  m1_1 : tree A
  o : option A
  m1_2 : tree A
  H : not_trivially_empty m1_1 o m1_2
  IHm1_1 : forall (m2 : tree B) (i : positive),
           get i
             (tree_rec (map_filter (fun b : B => f None (Some b)))
                (fun (l1 : tree A) (lrec : tree B -> tree C) 
                   (o1 : option A) (r1 : tree A) (rrec : tree B -> tree C) =>
                 tree_case
                   (map_filter (fun a : A => f (Some a) None) (Node l1 o1 r1))
                   (fun (l2 : tree B) (o2 : option B) (r2 : tree B) =>
                    Node (lrec l2) (f o1 o2) (rrec r2))) m1_1 m2) =
           f (get i m1_1) (get i m2)
  IHm1_2 : forall (m2 : tree B) (i : positive),
           get i
             (tree_rec (map_filter (fun b : B => f None (Some b)))
                (fun (l1 : tree A) (lrec : tree B -> tree C) 
                   (o1 : option A) (r1 : tree A) (rrec : tree B -> tree C) =>
                 tree_case
                   (map_filter (fun a : A => f (Some a) None) (Node l1 o1 r1))
                   (fun (l2 : tree B) (o2 : option B) (r2 : tree B) =>
                    Node (lrec l2) (f o1 o2) (rrec r2))) m1_2 m2) =
           f (get i m1_2) (get i m2)
  i : positive
  m2_1 : tree B
  o0 : option B
  m2_2 : tree B
  H0 : not_trivially_empty m2_1 o0 m2_2
  IHm2_1 : get (xI i)
             (tree_case
                (map_filter (fun a : A => f (Some a) None) (Node m1_1 o m1_2))
                (fun (l2 : tree B) (o2 : option B) (r2 : tree B) =>
                 Node
                   (tree_rec (map_filter (fun b : B => f None (Some b)))
                      (fun (l1 : tree A) (lrec : tree B -> tree C)
                         (o1 : option A) (r1 : tree A)
                         (rrec : tree B -> tree C) =>
                       tree_case
                         (map_filter (fun a : A => f (Some a) None)
                            (Node l1 o1 r1))
                         (fun (l3 : tree B) (o3 : option B) (r3 : tree B) =>
                          Node (lrec l3) (f o1 o3) (rrec r3))) m1_1 l2)
                   (f o o2)
                   (tree_rec (map_filter (fun b : B => f None (Some b)))
                      (fun (l1 : tree A) (lrec : tree B -> tree C)
                         (o1 : option A) (r1 : tree A)
                         (rrec : tree B -> tree C) =>
                       tree_case
                         (map_filter (fun a : A => f (Some a) None)
                            (Node l1 o1 r1))
                         (fun (l3 : tree B) (o3 : option B) (r3 : tree B) =>
                          Node (lrec l3) (f o1 o3) (rrec r3))) m1_2 r2)) m2_1) =
           f (get (xI i) (Node m1_1 o m1_2)) (get (xI i) m2_1)
  IHm2_2 : get (xI i)
             (tree_case
                (map_filter (fun a : A => f (Some a) None) (Node m1_1 o m1_2))
                (fun (l2 : tree B) (o2 : option B) (r2 : tree B) =>
                 Node
                   (tree_rec (map_filter (fun b : B => f None (Some b)))
                      (fun (l1 : tree A) (lrec : tree B -> tree C)
                         (o1 : option A) (r1 : tree A)
                         (rrec : tree B -> tree C) =>
                       tree_case
                         (map_filter (fun a : A => f (Some a) None)
                            (Node l1 o1 r1))
                         (fun (l3 : tree B) (o3 : option B) (r3 : tree B) =>
                          Node (lrec l3) (f o1 o3) (rrec r3))) m1_1 l2)
                   (f o o2)
                   (tree_rec (map_filter (fun b : B => f None (Some b)))
                      (fun (l1 : tree A) (lrec : tree B -> tree C)
                         (o1 : option A) (r1 : tree A)
                         (rrec : tree B -> tree C) =>
                       tree_case
                         (map_filter (fun a : A => f (Some a) None)
                            (Node l1 o1 r1))
                         (fun (l3 : tree B) (o3 : option B) (r3 : tree B) =>
                          Node (lrec l3) (f o1 o3) (rrec r3))) m1_2 r2)) m2_2) =
           f (get (xI i) (Node m1_1 o m1_2)) (get (xI i) m2_2)
  ============================
   (get i
      (tree_rec (map_filter (fun b : B => f None (Some b)))
         (fun (l1 : tree A) (lrec : tree B -> tree C) 
            (o1 : option A) (r1 : tree A) (rrec : tree B -> tree C) =>
          tree_case
            (map_filter (fun a : A => f (Some a) None) (Node l1 o1 r1))
            (fun (l2 : tree B) (o2 : option B) (r2 : tree B) =>
             Node (lrec l2) (f o1 o2) (rrec r2))) m1_2 m2_2) =
    f (get i m1_2) (get i m2_2))

  
  A : Type
  B : Type
  C : Type
  f : option A -> option B -> option C
  f_None_None : f None None = None
  m1_1 : tree A
  o : option A
  m1_2 : tree A
  H : not_trivially_empty m1_1 o m1_2
  IHm1_1 : forall (m2 : tree B) (i : positive),
           get i
             (tree_rec (map_filter (fun b : B => f None (Some b)))
                (fun (l1 : tree A) (lrec : tree B -> tree C) 
                   (o1 : option A) (r1 : tree A) (rrec : tree B -> tree C) =>
                 tree_case
                   (map_filter (fun a : A => f (Some a) None) (Node l1 o1 r1))
                   (fun (l2 : tree B) (o2 : option B) (r2 : tree B) =>
                    Node (lrec l2) (f o1 o2) (rrec r2))) m1_1 m2) =
           f (get i m1_1) (get i m2)
  IHm1_2 : forall (m2 : tree B) (i : positive),
           get i
             (tree_rec (map_filter (fun b : B => f None (Some b)))
                (fun (l1 : tree A) (lrec : tree B -> tree C) 
                   (o1 : option A) (r1 : tree A) (rrec : tree B -> tree C) =>
                 tree_case
                   (map_filter (fun a : A => f (Some a) None) (Node l1 o1 r1))
                   (fun (l2 : tree B) (o2 : option B) (r2 : tree B) =>
                    Node (lrec l2) (f o1 o2) (rrec r2))) m1_2 m2) =
           f (get i m1_2) (get i m2)
  i : positive
  m2_1 : tree B
  o0 : option B
  m2_2 : tree B
  H0 : not_trivially_empty m2_1 o0 m2_2
  IHm2_1 : get (xO i)
             (tree_case
                (map_filter (fun a : A => f (Some a) None) (Node m1_1 o m1_2))
                (fun (l2 : tree B) (o2 : option B) (r2 : tree B) =>
                 Node
                   (tree_rec (map_filter (fun b : B => f None (Some b)))
                      (fun (l1 : tree A) (lrec : tree B -> tree C)
                         (o1 : option A) (r1 : tree A)
                         (rrec : tree B -> tree C) =>
                       tree_case
                         (map_filter (fun a : A => f (Some a) None)
                            (Node l1 o1 r1))
                         (fun (l3 : tree B) (o3 : option B) (r3 : tree B) =>
                          Node (lrec l3) (f o1 o3) (rrec r3))) m1_1 l2)
                   (f o o2)
                   (tree_rec (map_filter (fun b : B => f None (Some b)))
                      (fun (l1 : tree A) (lrec : tree B -> tree C)
                         (o1 : option A) (r1 : tree A)
                         (rrec : tree B -> tree C) =>
                       tree_case
                         (map_filter (fun a : A => f (Some a) None)
                            (Node l1 o1 r1))
                         (fun (l3 : tree B) (o3 : option B) (r3 : tree B) =>
                          Node (lrec l3) (f o1 o3) (rrec r3))) m1_2 r2)) m2_1) =
           f (get (xO i) (Node m1_1 o m1_2)) (get (xO i) m2_1)
  IHm2_2 : get (xO i)
             (tree_case
                (map_filter (fun a : A => f (Some a) None) (Node m1_1 o m1_2))
                (fun (l2 : tree B) (o2 : option B) (r2 : tree B) =>
                 Node
                   (tree_rec (map_filter (fun b : B => f None (Some b)))
                      (fun (l1 : tree A) (lrec : tree B -> tree C)
                         (o1 : option A) (r1 : tree A)
                         (rrec : tree B -> tree C) =>
                       tree_case
                         (map_filter (fun a : A => f (Some a) None)
                            (Node l1 o1 r1))
                         (fun (l3 : tree B) (o3 : option B) (r3 : tree B) =>
                          Node (lrec l3) (f o1 o3) (rrec r3))) m1_1 l2)
                   (f o o2)
                   (tree_rec (map_filter (fun b : B => f None (Some b)))
                      (fun (l1 : tree A) (lrec : tree B -> tree C)
                         (o1 : option A) (r1 : tree A)
                         (rrec : tree B -> tree C) =>
                       tree_case
                         (map_filter (fun a : A => f (Some a) None)
                            (Node l1 o1 r1))
                         (fun (l3 : tree B) (o3 : option B) (r3 : tree B) =>
                          Node (lrec l3) (f o1 o3) (rrec r3))) m1_2 r2)) m2_2) =
           f (get (xO i) (Node m1_1 o m1_2)) (get (xO i) m2_2)
  ============================
   (get i
      (tree_rec (map_filter (fun b : B => f None (Some b)))
         (fun (l1 : tree A) (lrec : tree B -> tree C) 
            (o1 : option A) (r1 : tree A) (rrec : tree B -> tree C) =>
          tree_case
            (map_filter (fun a : A => f (Some a) None) (Node l1 o1 r1))
            (fun (l2 : tree B) (o2 : option B) (r2 : tree B) =>
             Node (lrec l2) (f o1 o2) (rrec r2))) m1_1 m2_1) =
    f (get i m1_1) (get i m2_1))

  
  A : Type
  B : Type
  C : Type
  f : option A -> option B -> option C
  f_None_None : f None None = None
  m1_1 : tree A
  o : option A
  m1_2 : tree A
  H : not_trivially_empty m1_1 o m1_2
  IHm1_1 : forall (m2 : tree B) (i : positive),
           get i
             (tree_rec (map_filter (fun b : B => f None (Some b)))
                (fun (l1 : tree A) (lrec : tree B -> tree C) 
                   (o1 : option A) (r1 : tree A) (rrec : tree B -> tree C) =>
                 tree_case
                   (map_filter (fun a : A => f (Some a) None) (Node l1 o1 r1))
                   (fun (l2 : tree B) (o2 : option B) (r2 : tree B) =>
                    Node (lrec l2) (f o1 o2) (rrec r2))) m1_1 m2) =
           f (get i m1_1) (get i m2)
  IHm1_2 : forall (m2 : tree B) (i : positive),
           get i
             (tree_rec (map_filter (fun b : B => f None (Some b)))
                (fun (l1 : tree A) (lrec : tree B -> tree C) 
                   (o1 : option A) (r1 : tree A) (rrec : tree B -> tree C) =>
                 tree_case
                   (map_filter (fun a : A => f (Some a) None) (Node l1 o1 r1))
                   (fun (l2 : tree B) (o2 : option B) (r2 : tree B) =>
                    Node (lrec l2) (f o1 o2) (rrec r2))) m1_2 m2) =
           f (get i m1_2) (get i m2)
  m2_1 : tree B
  o0 : option B
  m2_2 : tree B
  H0 : not_trivially_empty m2_1 o0 m2_2
  IHm2_1 : get xH
             (tree_case
                (map_filter (fun a : A => f (Some a) None) (Node m1_1 o m1_2))
                (fun (l2 : tree B) (o2 : option B) (r2 : tree B) =>
                 Node
                   (tree_rec (map_filter (fun b : B => f None (Some b)))
                      (fun (l1 : tree A) (lrec : tree B -> tree C)
                         (o1 : option A) (r1 : tree A)
                         (rrec : tree B -> tree C) =>
                       tree_case
                         (map_filter (fun a : A => f (Some a) None)
                            (Node l1 o1 r1))
                         (fun (l3 : tree B) (o3 : option B) (r3 : tree B) =>
                          Node (lrec l3) (f o1 o3) (rrec r3))) m1_1 l2)
                   (f o o2)
                   (tree_rec (map_filter (fun b : B => f None (Some b)))
                      (fun (l1 : tree A) (lrec : tree B -> tree C)
                         (o1 : option A) (r1 : tree A)
                         (rrec : tree B -> tree C) =>
                       tree_case
                         (map_filter (fun a : A => f (Some a) None)
                            (Node l1 o1 r1))
                         (fun (l3 : tree B) (o3 : option B) (r3 : tree B) =>
                          Node (lrec l3) (f o1 o3) (rrec r3))) m1_2 r2)) m2_1) =
           f (get xH (Node m1_1 o m1_2)) (get xH m2_1)
  IHm2_2 : get xH
             (tree_case
                (map_filter (fun a : A => f (Some a) None) (Node m1_1 o m1_2))
                (fun (l2 : tree B) (o2 : option B) (r2 : tree B) =>
                 Node
                   (tree_rec (map_filter (fun b : B => f None (Some b)))
                      (fun (l1 : tree A) (lrec : tree B -> tree C)
                         (o1 : option A) (r1 : tree A)
                         (rrec : tree B -> tree C) =>
                       tree_case
                         (map_filter (fun a : A => f (Some a) None)
                            (Node l1 o1 r1))
                         (fun (l3 : tree B) (o3 : option B) (r3 : tree B) =>
                          Node (lrec l3) (f o1 o3) (rrec r3))) m1_1 l2)
                   (f o o2)
                   (tree_rec (map_filter (fun b : B => f None (Some b)))
                      (fun (l1 : tree A) (lrec : tree B -> tree C)
                         (o1 : option A) (r1 : tree A)
                         (rrec : tree B -> tree C) =>
                       tree_case
                         (map_filter (fun a : A => f (Some a) None)
                            (Node l1 o1 r1))
                         (fun (l3 : tree B) (o3 : option B) (r3 : tree B) =>
                          Node (lrec l3) (f o1 o3) (rrec r3))) m1_2 r2)) m2_2) =
           f (get xH (Node m1_1 o m1_2)) (get xH m2_2)
  ============================
   (f o o0 = f o o0)


DEBUG:Going to execute:
auto
DEBUG LTAC Evaluated term: i

Goals:
  
  A : Type
  B : Type
  C : Type
  f : option A -> option B -> option C
  f_None_None : f None None = None
  m1_1 : tree A
  o : option A
  m1_2 : tree A
  H : not_trivially_empty m1_1 o m1_2
  IHm1_1 : forall (m2 : tree B) (i : positive),
           get i
             (tree_rec (map_filter (fun b : B => f None (Some b)))
                (fun (l1 : tree A) (lrec : tree B -> tree C) 
                   (o1 : option A) (r1 : tree A) (rrec : tree B -> tree C) =>
                 tree_case
                   (map_filter (fun a : A => f (Some a) None) (Node l1 o1 r1))
                   (fun (l2 : tree B) (o2 : option B) (r2 : tree B) =>
                    Node (lrec l2) (f o1 o2) (rrec r2))) m1_1 m2) =
           f (get i m1_1) (get i m2)
  IHm1_2 : forall (m2 : tree B) (i : positive),
           get i
             (tree_rec (map_filter (fun b : B => f None (Some b)))
                (fun (l1 : tree A) (lrec : tree B -> tree C) 
                   (o1 : option A) (r1 : tree A) (rrec : tree B -> tree C) =>
                 tree_case
                   (map_filter (fun a : A => f (Some a) None) (Node l1 o1 r1))
                   (fun (l2 : tree B) (o2 : option B) (r2 : tree B) =>
                    Node (lrec l2) (f o1 o2) (rrec r2))) m1_2 m2) =
           f (get i m1_2) (get i m2)
  i : positive
  m2_1 : tree B
  o0 : option B
  m2_2 : tree B
  H0 : not_trivially_empty m2_1 o0 m2_2
  IHm2_1 : get (xI i)
             (tree_case
                (map_filter (fun a : A => f (Some a) None) (Node m1_1 o m1_2))
                (fun (l2 : tree B) (o2 : option B) (r2 : tree B) =>
                 Node
                   (tree_rec (map_filter (fun b : B => f None (Some b)))
                      (fun (l1 : tree A) (lrec : tree B -> tree C)
                         (o1 : option A) (r1 : tree A)
                         (rrec : tree B -> tree C) =>
                       tree_case
                         (map_filter (fun a : A => f (Some a) None)
                            (Node l1 o1 r1))
                         (fun (l3 : tree B) (o3 : option B) (r3 : tree B) =>
                          Node (lrec l3) (f o1 o3) (rrec r3))) m1_1 l2)
                   (f o o2)
                   (tree_rec (map_filter (fun b : B => f None (Some b)))
                      (fun (l1 : tree A) (lrec : tree B -> tree C)
                         (o1 : option A) (r1 : tree A)
                         (rrec : tree B -> tree C) =>
                       tree_case
                         (map_filter (fun a : A => f (Some a) None)
                            (Node l1 o1 r1))
                         (fun (l3 : tree B) (o3 : option B) (r3 : tree B) =>
                          Node (lrec l3) (f o1 o3) (rrec r3))) m1_2 r2)) m2_1) =
           f (get (xI i) (Node m1_1 o m1_2)) (get (xI i) m2_1)
  IHm2_2 : get (xI i)
             (tree_case
                (map_filter (fun a : A => f (Some a) None) (Node m1_1 o m1_2))
                (fun (l2 : tree B) (o2 : option B) (r2 : tree B) =>
                 Node
                   (tree_rec (map_filter (fun b : B => f None (Some b)))
                      (fun (l1 : tree A) (lrec : tree B -> tree C)
                         (o1 : option A) (r1 : tree A)
                         (rrec : tree B -> tree C) =>
                       tree_case
                         (map_filter (fun a : A => f (Some a) None)
                            (Node l1 o1 r1))
                         (fun (l3 : tree B) (o3 : option B) (r3 : tree B) =>
                          Node (lrec l3) (f o1 o3) (rrec r3))) m1_1 l2)
                   (f o o2)
                   (tree_rec (map_filter (fun b : B => f None (Some b)))
                      (fun (l1 : tree A) (lrec : tree B -> tree C)
                         (o1 : option A) (r1 : tree A)
                         (rrec : tree B -> tree C) =>
                       tree_case
                         (map_filter (fun a : A => f (Some a) None)
                            (Node l1 o1 r1))
                         (fun (l3 : tree B) (o3 : option B) (r3 : tree B) =>
                          Node (lrec l3) (f o1 o3) (rrec r3))) m1_2 r2)) m2_2) =
           f (get (xI i) (Node m1_1 o m1_2)) (get (xI i) m2_2)
  ============================
   (get i
      (tree_rec (map_filter (fun b : B => f None (Some b)))
         (fun (l1 : tree A) (lrec : tree B -> tree C) 
            (o1 : option A) (r1 : tree A) (rrec : tree B -> tree C) =>
          tree_case
            (map_filter (fun a : A => f (Some a) None) (Node l1 o1 r1))
            (fun (l2 : tree B) (o2 : option B) (r2 : tree B) =>
             Node (lrec l2) (f o1 o2) (rrec r2))) m1_2 m2_2) =
    f (get i m1_2) (get i m2_2))

  
  A : Type
  B : Type
  C : Type
  f : option A -> option B -> option C
  f_None_None : f None None = None
  m1_1 : tree A
  o : option A
  m1_2 : tree A
  H : not_trivially_empty m1_1 o m1_2
  IHm1_1 : forall (m2 : tree B) (i : positive),
           get i
             (tree_rec (map_filter (fun b : B => f None (Some b)))
                (fun (l1 : tree A) (lrec : tree B -> tree C) 
                   (o1 : option A) (r1 : tree A) (rrec : tree B -> tree C) =>
                 tree_case
                   (map_filter (fun a : A => f (Some a) None) (Node l1 o1 r1))
                   (fun (l2 : tree B) (o2 : option B) (r2 : tree B) =>
                    Node (lrec l2) (f o1 o2) (rrec r2))) m1_1 m2) =
           f (get i m1_1) (get i m2)
  IHm1_2 : forall (m2 : tree B) (i : positive),
           get i
             (tree_rec (map_filter (fun b : B => f None (Some b)))
                (fun (l1 : tree A) (lrec : tree B -> tree C) 
                   (o1 : option A) (r1 : tree A) (rrec : tree B -> tree C) =>
                 tree_case
                   (map_filter (fun a : A => f (Some a) None) (Node l1 o1 r1))
                   (fun (l2 : tree B) (o2 : option B) (r2 : tree B) =>
                    Node (lrec l2) (f o1 o2) (rrec r2))) m1_2 m2) =
           f (get i m1_2) (get i m2)
  i : positive
  m2_1 : tree B
  o0 : option B
  m2_2 : tree B
  H0 : not_trivially_empty m2_1 o0 m2_2
  IHm2_1 : get (xO i)
             (tree_case
                (map_filter (fun a : A => f (Some a) None) (Node m1_1 o m1_2))
                (fun (l2 : tree B) (o2 : option B) (r2 : tree B) =>
                 Node
                   (tree_rec (map_filter (fun b : B => f None (Some b)))
                      (fun (l1 : tree A) (lrec : tree B -> tree C)
                         (o1 : option A) (r1 : tree A)
                         (rrec : tree B -> tree C) =>
                       tree_case
                         (map_filter (fun a : A => f (Some a) None)
                            (Node l1 o1 r1))
                         (fun (l3 : tree B) (o3 : option B) (r3 : tree B) =>
                          Node (lrec l3) (f o1 o3) (rrec r3))) m1_1 l2)
                   (f o o2)
                   (tree_rec (map_filter (fun b : B => f None (Some b)))
                      (fun (l1 : tree A) (lrec : tree B -> tree C)
                         (o1 : option A) (r1 : tree A)
                         (rrec : tree B -> tree C) =>
                       tree_case
                         (map_filter (fun a : A => f (Some a) None)
                            (Node l1 o1 r1))
                         (fun (l3 : tree B) (o3 : option B) (r3 : tree B) =>
                          Node (lrec l3) (f o1 o3) (rrec r3))) m1_2 r2)) m2_1) =
           f (get (xO i) (Node m1_1 o m1_2)) (get (xO i) m2_1)
  IHm2_2 : get (xO i)
             (tree_case
                (map_filter (fun a : A => f (Some a) None) (Node m1_1 o m1_2))
                (fun (l2 : tree B) (o2 : option B) (r2 : tree B) =>
                 Node
                   (tree_rec (map_filter (fun b : B => f None (Some b)))
                      (fun (l1 : tree A) (lrec : tree B -> tree C)
                         (o1 : option A) (r1 : tree A)
                         (rrec : tree B -> tree C) =>
                       tree_case
                         (map_filter (fun a : A => f (Some a) None)
                            (Node l1 o1 r1))
                         (fun (l3 : tree B) (o3 : option B) (r3 : tree B) =>
                          Node (lrec l3) (f o1 o3) (rrec r3))) m1_1 l2)
                   (f o o2)
                   (tree_rec (map_filter (fun b : B => f None (Some b)))
                      (fun (l1 : tree A) (lrec : tree B -> tree C)
                         (o1 : option A) (r1 : tree A)
                         (rrec : tree B -> tree C) =>
                       tree_case
                         (map_filter (fun a : A => f (Some a) None)
                            (Node l1 o1 r1))
                         (fun (l3 : tree B) (o3 : option B) (r3 : tree B) =>
                          Node (lrec l3) (f o1 o3) (rrec r3))) m1_2 r2)) m2_2) =
           f (get (xO i) (Node m1_1 o m1_2)) (get (xO i) m2_2)
  ============================
   (get i
      (tree_rec (map_filter (fun b : B => f None (Some b)))
         (fun (l1 : tree A) (lrec : tree B -> tree C) 
            (o1 : option A) (r1 : tree A) (rrec : tree B -> tree C) =>
          tree_case
            (map_filter (fun a : A => f (Some a) None) (Node l1 o1 r1))
            (fun (l2 : tree B) (o2 : option B) (r2 : tree B) =>
             Node (lrec l2) (f o1 o2) (rrec r2))) m1_1 m2_1) =
    f (get i m1_1) (get i m2_1))

  
  A : Type
  B : Type
  C : Type
  f : option A -> option B -> option C
  f_None_None : f None None = None
  m1_1 : tree A
  o : option A
  m1_2 : tree A
  H : not_trivially_empty m1_1 o m1_2
  IHm1_1 : forall (m2 : tree B) (i : positive),
           get i
             (tree_rec (map_filter (fun b : B => f None (Some b)))
                (fun (l1 : tree A) (lrec : tree B -> tree C) 
                   (o1 : option A) (r1 : tree A) (rrec : tree B -> tree C) =>
                 tree_case
                   (map_filter (fun a : A => f (Some a) None) (Node l1 o1 r1))
                   (fun (l2 : tree B) (o2 : option B) (r2 : tree B) =>
                    Node (lrec l2) (f o1 o2) (rrec r2))) m1_1 m2) =
           f (get i m1_1) (get i m2)
  IHm1_2 : forall (m2 : tree B) (i : positive),
           get i
             (tree_rec (map_filter (fun b : B => f None (Some b)))
                (fun (l1 : tree A) (lrec : tree B -> tree C) 
                   (o1 : option A) (r1 : tree A) (rrec : tree B -> tree C) =>
                 tree_case
                   (map_filter (fun a : A => f (Some a) None) (Node l1 o1 r1))
                   (fun (l2 : tree B) (o2 : option B) (r2 : tree B) =>
                    Node (lrec l2) (f o1 o2) (rrec r2))) m1_2 m2) =
           f (get i m1_2) (get i m2)
  m2_1 : tree B
  o0 : option B
  m2_2 : tree B
  H0 : not_trivially_empty m2_1 o0 m2_2
  IHm2_1 : get xH
             (tree_case
                (map_filter (fun a : A => f (Some a) None) (Node m1_1 o m1_2))
                (fun (l2 : tree B) (o2 : option B) (r2 : tree B) =>
                 Node
                   (tree_rec (map_filter (fun b : B => f None (Some b)))
                      (fun (l1 : tree A) (lrec : tree B -> tree C)
                         (o1 : option A) (r1 : tree A)
                         (rrec : tree B -> tree C) =>
                       tree_case
                         (map_filter (fun a : A => f (Some a) None)
                            (Node l1 o1 r1))
                         (fun (l3 : tree B) (o3 : option B) (r3 : tree B) =>
                          Node (lrec l3) (f o1 o3) (rrec r3))) m1_1 l2)
                   (f o o2)
                   (tree_rec (map_filter (fun b : B => f None (Some b)))
                      (fun (l1 : tree A) (lrec : tree B -> tree C)
                         (o1 : option A) (r1 : tree A)
                         (rrec : tree B -> tree C) =>
                       tree_case
                         (map_filter (fun a : A => f (Some a) None)
                            (Node l1 o1 r1))
                         (fun (l3 : tree B) (o3 : option B) (r3 : tree B) =>
                          Node (lrec l3) (f o1 o3) (rrec r3))) m1_2 r2)) m2_1) =
           f (get xH (Node m1_1 o m1_2)) (get xH m2_1)
  IHm2_2 : get xH
             (tree_case
                (map_filter (fun a : A => f (Some a) None) (Node m1_1 o m1_2))
                (fun (l2 : tree B) (o2 : option B) (r2 : tree B) =>
                 Node
                   (tree_rec (map_filter (fun b : B => f None (Some b)))
                      (fun (l1 : tree A) (lrec : tree B -> tree C)
                         (o1 : option A) (r1 : tree A)
                         (rrec : tree B -> tree C) =>
                       tree_case
                         (map_filter (fun a : A => f (Some a) None)
                            (Node l1 o1 r1))
                         (fun (l3 : tree B) (o3 : option B) (r3 : tree B) =>
                          Node (lrec l3) (f o1 o3) (rrec r3))) m1_1 l2)
                   (f o o2)
                   (tree_rec (map_filter (fun b : B => f None (Some b)))
                      (fun (l1 : tree A) (lrec : tree B -> tree C)
                         (o1 : option A) (r1 : tree A)
                         (rrec : tree B -> tree C) =>
                       tree_case
                         (map_filter (fun a : A => f (Some a) None)
                            (Node l1 o1 r1))
                         (fun (l3 : tree B) (o3 : option B) (r3 : tree B) =>
                          Node (lrec l3) (f o1 o3) (rrec r3))) m1_2 r2)) m2_2) =
           f (get xH (Node m1_1 o m1_2)) (get xH m2_2)
  ============================
   (f o o0 = f o o0)


DEBUG:Going to execute:
<coq-core.plugins.ltac::auto@0> $1 $2 $3