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)
  m2 : tree B
  i : positive
  ============================
   (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) =
    f (get i (Node m1_1 o m1_2)) (get i m2))


DEBUG:Going to execute:
induction m2 using tree_ind
DEBUG LTAC Evaluated term: unroll_tree_rec

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
  ============================
   (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)) Empty) =
    f (get i (Node m1_1 o m1_2)) (get i Empty))

  
  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)
  ============================
   (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))
         (Node m2_1 o0 m2_2)) =
    f (get i (Node m1_1 o m1_2)) (get i (Node m2_1 o0 m2_2)))


DEBUG:Going to execute:
intros
DEBUG LTAC Evaluated term: tree_ind
DEBUG LTAC Evaluated term: m2