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
  ============================
   (option_map (fun a : A => f (Some a) None) (get i (Node m1_1 o m1_2)) =
    f (get i (Node m1_1 o m1_2)) None)


DEBUG:Going to execute:
destruct (get i (Node m1_1 o m1_2))
DEBUG LTAC Evaluated term: gmap_filter
DEBUG LTAC Evaluated term: gmap_filter

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
  a : A
  ============================
   (option_map (fun a : A => f (Some a) None) (Some a) = f (Some a) None)

  
  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
  ============================
   (option_map (fun a : A => f (Some a) None) None = f None None)


DEBUG:Going to execute:
auto
DEBUG LTAC Evaluated term: (get i (Node m1_1 o m1_2))

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
  a : A
  ============================
   (option_map (fun a : A => f (Some a) None) (Some a) = f (Some a) None)

  
  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
  ============================
   (option_map (fun a : A => f (Some a) None) None = f None None)


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