Goal:
  
  A : Type
  B : Type
  C : Type
  f : option A -> option B -> option C
  f_None_None : f None None = None
  ============================
   (forall (m1 : tree A) (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 m2) =
    f (get i m1) (get i m2))


DEBUG:Going to execute:
induction m1 using tree_ind
DEBUG LTAC Evaluated term: gcombine'_r
DEBUG LTAC Evaluated term: gcombine'_l
DEBUG LTAC Evaluated term: gcombine'_by_tac
DEBUG LTAC Evaluated term: combine_view
DEBUG LTAC Evaluated term: combine_view_gen

Goals:
  
  A : Type
  B : Type
  C : Type
  f : option A -> option B -> option C
  f_None_None : f None None = None
  ============================
   (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))) Empty m2) =
    f (get i Empty) (get i m2))

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


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