Goal:
    A : Type  B : Type
  ============================
   (forall (f : A -> option B) (m : tree' A) (i : positive),
    get i (map_filter' f m) = option_map f (get' i m))


DEBUG:Going to execute:
induction m

Goals:
  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  ============================
   (forall i : positive,
    get i (map_filter' f (Node001 m)) = option_map f (get' i (Node001 m)))

    A : Type  B : Type  f : A -> option B  a : A
  ============================
   (forall i : positive,
    get i (map_filter' f (Node010 a)) = option_map f (get' i (Node010 a)))

  
  A : Type
  B : Type
  f : A -> option B
  a : A
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  ============================
   (forall i : positive,
    get i (map_filter' f (Node011 a m)) = option_map f (get' i (Node011 a m)))

  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  ============================
   (forall i : positive,
    get i (map_filter' f (Node100 m)) = option_map f (get' i (Node100 m)))

  
  A : Type
  B : Type
  f : A -> option B
  m1 : tree' A
  m2 : tree' A
  IHm1 : forall i : positive,
         get i (map_filter' f m1) = option_map f (get' i m1)
  IHm2 : forall i : positive,
         get i (map_filter' f m2) = option_map f (get' i m2)
  ============================
   (forall i : positive,
    get i (map_filter' f (Node101 m1 m2)) =
    option_map f (get' i (Node101 m1 m2)))

  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  a : A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  ============================
   (forall i : positive,
    get i (map_filter' f (Node110 m a)) = option_map f (get' i (Node110 m a)))

  
  A : Type
  B : Type
  f : A -> option B
  m1 : tree' A
  a : A
  m2 : tree' A
  IHm1 : forall i : positive,
         get i (map_filter' f m1) = option_map f (get' i m1)
  IHm2 : forall i : positive,
         get i (map_filter' f m2) = option_map f (get' i m2)
  ============================
   (forall i : positive,
    get i (map_filter' f (Node111 m1 a m2)) =
    option_map f (get' i (Node111 m1 a m2)))


DEBUG:Going to execute:
simpl

Goals:
  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  ============================
   (forall i : positive,
    get i (Node Empty None (map_filter' f m)) =
    option_map f (get' i (Node001 m)))

    A : Type  B : Type  f : A -> option B  a : A
  ============================
   (forall i : positive,
    get i (Node Empty (f a) Empty) = option_map f (get' i (Node010 a)))

  
  A : Type
  B : Type
  f : A -> option B
  a : A
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  ============================
   (forall i : positive,
    get i (Node Empty (f a) (map_filter' f m)) =
    option_map f (get' i (Node011 a m)))

  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  ============================
   (forall i : positive,
    get i (Node (map_filter' f m) None Empty) =
    option_map f (get' i (Node100 m)))

  
  A : Type
  B : Type
  f : A -> option B
  m1 : tree' A
  m2 : tree' A
  IHm1 : forall i : positive,
         get i (map_filter' f m1) = option_map f (get' i m1)
  IHm2 : forall i : positive,
         get i (map_filter' f m2) = option_map f (get' i m2)
  ============================
   (forall i : positive,
    get i (Node (map_filter' f m1) None (map_filter' f m2)) =
    option_map f (get' i (Node101 m1 m2)))

  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  a : A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  ============================
   (forall i : positive,
    get i (Node (map_filter' f m) (f a) Empty) =
    option_map f (get' i (Node110 m a)))

  
  A : Type
  B : Type
  f : A -> option B
  m1 : tree' A
  a : A
  m2 : tree' A
  IHm1 : forall i : positive,
         get i (map_filter' f m1) = option_map f (get' i m1)
  IHm2 : forall i : positive,
         get i (map_filter' f m2) = option_map f (get' i m2)
  ============================
   (forall i : positive,
    get i (Node (map_filter' f m1) (f a) (map_filter' f m2)) =
    option_map f (get' i (Node111 m1 a m2)))


DEBUG:Going to execute:
intros

Goals:
  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  i : positive
  ============================
   (get i (Node Empty None (map_filter' f m)) =
    option_map f (get' i (Node001 m)))

    A : Type  B : Type  f : A -> option B  a : A  i : positive
  ============================
   (get i (Node Empty (f a) Empty) = option_map f (get' i (Node010 a)))

  
  A : Type
  B : Type
  f : A -> option B
  a : A
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  i : positive
  ============================
   (get i (Node Empty (f a) (map_filter' f m)) =
    option_map f (get' i (Node011 a m)))

  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  i : positive
  ============================
   (get i (Node (map_filter' f m) None Empty) =
    option_map f (get' i (Node100 m)))

  
  A : Type
  B : Type
  f : A -> option B
  m1 : tree' A
  m2 : tree' A
  IHm1 : forall i : positive,
         get i (map_filter' f m1) = option_map f (get' i m1)
  IHm2 : forall i : positive,
         get i (map_filter' f m2) = option_map f (get' i m2)
  i : positive
  ============================
   (get i (Node (map_filter' f m1) None (map_filter' f m2)) =
    option_map f (get' i (Node101 m1 m2)))

  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  a : A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  i : positive
  ============================
   (get i (Node (map_filter' f m) (f a) Empty) =
    option_map f (get' i (Node110 m a)))

  
  A : Type
  B : Type
  f : A -> option B
  m1 : tree' A
  a : A
  m2 : tree' A
  IHm1 : forall i : positive,
         get i (map_filter' f m1) = option_map f (get' i m1)
  IHm2 : forall i : positive,
         get i (map_filter' f m2) = option_map f (get' i m2)
  i : positive
  ============================
   (get i (Node (map_filter' f m1) (f a) (map_filter' f m2)) =
    option_map f (get' i (Node111 m1 a m2)))


DEBUG:Going to execute:
rewrite gNode

Goals:
  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  i : positive
  ============================
   (match i with
    | xI j => get j (map_filter' f m)
    | xO j => get j Empty
    | xH => None
    end = option_map f (get' i (Node001 m)))

    A : Type  B : Type  f : A -> option B  a : A  i : positive
  ============================
   (match i with
    | xI j | xO j => get j Empty
    | xH => f a
    end = option_map f (get' i (Node010 a)))

  
  A : Type
  B : Type
  f : A -> option B
  a : A
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  i : positive
  ============================
   (match i with
    | xI j => get j (map_filter' f m)
    | xO j => get j Empty
    | xH => f a
    end = option_map f (get' i (Node011 a m)))

  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  i : positive
  ============================
   (match i with
    | xI j => get j Empty
    | xO j => get j (map_filter' f m)
    | xH => None
    end = option_map f (get' i (Node100 m)))

  
  A : Type
  B : Type
  f : A -> option B
  m1 : tree' A
  m2 : tree' A
  IHm1 : forall i : positive,
         get i (map_filter' f m1) = option_map f (get' i m1)
  IHm2 : forall i : positive,
         get i (map_filter' f m2) = option_map f (get' i m2)
  i : positive
  ============================
   (match i with
    | xI j => get j (map_filter' f m2)
    | xO j => get j (map_filter' f m1)
    | xH => None
    end = option_map f (get' i (Node101 m1 m2)))

  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  a : A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  i : positive
  ============================
   (match i with
    | xI j => get j Empty
    | xO j => get j (map_filter' f m)
    | xH => f a
    end = option_map f (get' i (Node110 m a)))

  
  A : Type
  B : Type
  f : A -> option B
  m1 : tree' A
  a : A
  m2 : tree' A
  IHm1 : forall i : positive,
         get i (map_filter' f m1) = option_map f (get' i m1)
  IHm2 : forall i : positive,
         get i (map_filter' f m2) = option_map f (get' i m2)
  i : positive
  ============================
   (match i with
    | xI j => get j (map_filter' f m2)
    | xO j => get j (map_filter' f m1)
    | xH => f a
    end = option_map f (get' i (Node111 m1 a m2)))


DEBUG:Going to execute:
destruct i
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
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
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
  f : A -> option B
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  i : positive
  ============================
   (get i (map_filter' f m) = option_map f (get' (xI i) (Node001 m)))

  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  i : positive
  ============================
   (get i Empty = option_map f (get' (xO i) (Node001 m)))

  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  ============================
   (None = option_map f (get' xH (Node001 m)))

    A : Type  B : Type  f : A -> option B  a : A  i : positive
  ============================
   (get i Empty = option_map f (get' (xI i) (Node010 a)))

    A : Type  B : Type  f : A -> option B  a : A  i : positive
  ============================
   (get i Empty = option_map f (get' (xO i) (Node010 a)))

    A : Type  B : Type  f : A -> option B  a : A
  ============================
   (f a = option_map f (get' xH (Node010 a)))

  
  A : Type
  B : Type
  f : A -> option B
  a : A
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  i : positive
  ============================
   (get i (map_filter' f m) = option_map f (get' (xI i) (Node011 a m)))

  
  A : Type
  B : Type
  f : A -> option B
  a : A
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  i : positive
  ============================
   (get i Empty = option_map f (get' (xO i) (Node011 a m)))

  
  A : Type
  B : Type
  f : A -> option B
  a : A
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  ============================
   (f a = option_map f (get' xH (Node011 a m)))

  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  i : positive
  ============================
   (get i Empty = option_map f (get' (xI i) (Node100 m)))

  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  i : positive
  ============================
   (get i (map_filter' f m) = option_map f (get' (xO i) (Node100 m)))

  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  ============================
   (None = option_map f (get' xH (Node100 m)))

  
  A : Type
  B : Type
  f : A -> option B
  m1 : tree' A
  m2 : tree' A
  IHm1 : forall i : positive,
         get i (map_filter' f m1) = option_map f (get' i m1)
  IHm2 : forall i : positive,
         get i (map_filter' f m2) = option_map f (get' i m2)
  i : positive
  ============================
   (get i (map_filter' f m2) = option_map f (get' (xI i) (Node101 m1 m2)))

  
  A : Type
  B : Type
  f : A -> option B
  m1 : tree' A
  m2 : tree' A
  IHm1 : forall i : positive,
         get i (map_filter' f m1) = option_map f (get' i m1)
  IHm2 : forall i : positive,
         get i (map_filter' f m2) = option_map f (get' i m2)
  i : positive
  ============================
   (get i (map_filter' f m1) = option_map f (get' (xO i) (Node101 m1 m2)))

  
  A : Type
  B : Type
  f : A -> option B
  m1 : tree' A
  m2 : tree' A
  IHm1 : forall i : positive,
         get i (map_filter' f m1) = option_map f (get' i m1)
  IHm2 : forall i : positive,
         get i (map_filter' f m2) = option_map f (get' i m2)
  ============================
   (None = option_map f (get' xH (Node101 m1 m2)))

  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  a : A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  i : positive
  ============================
   (get i Empty = option_map f (get' (xI i) (Node110 m a)))

  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  a : A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  i : positive
  ============================
   (get i (map_filter' f m) = option_map f (get' (xO i) (Node110 m a)))

  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  a : A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  ============================
   (f a = option_map f (get' xH (Node110 m a)))

  
  A : Type
  B : Type
  f : A -> option B
  m1 : tree' A
  a : A
  m2 : tree' A
  IHm1 : forall i : positive,
         get i (map_filter' f m1) = option_map f (get' i m1)
  IHm2 : forall i : positive,
         get i (map_filter' f m2) = option_map f (get' i m2)
  i : positive
  ============================
   (get i (map_filter' f m2) = option_map f (get' (xI i) (Node111 m1 a m2)))

  
  A : Type
  B : Type
  f : A -> option B
  m1 : tree' A
  a : A
  m2 : tree' A
  IHm1 : forall i : positive,
         get i (map_filter' f m1) = option_map f (get' i m1)
  IHm2 : forall i : positive,
         get i (map_filter' f m2) = option_map f (get' i m2)
  i : positive
  ============================
   (get i (map_filter' f m1) = option_map f (get' (xO i) (Node111 m1 a m2)))

  
  A : Type
  B : Type
  f : A -> option B
  m1 : tree' A
  a : A
  m2 : tree' A
  IHm1 : forall i : positive,
         get i (map_filter' f m1) = option_map f (get' i m1)
  IHm2 : forall i : positive,
         get i (map_filter' f m2) = option_map f (get' i m2)
  ============================
   (f a = option_map f (get' xH (Node111 m1 a m2)))


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

Goals:
  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  i : positive
  ============================
   (get i (map_filter' f m) = option_map f (get' i m))

  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  i : positive
  ============================
   (None = None)

  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  ============================
   (None = None)

    A : Type  B : Type  f : A -> option B  a : A  i : positive
  ============================
   (None = None)

    A : Type  B : Type  f : A -> option B  a : A  i : positive
  ============================
   (None = None)

    A : Type  B : Type  f : A -> option B  a : A
  ============================
   (f a = f a)

  
  A : Type
  B : Type
  f : A -> option B
  a : A
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  i : positive
  ============================
   (get i (map_filter' f m) = option_map f (get' i m))

  
  A : Type
  B : Type
  f : A -> option B
  a : A
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  i : positive
  ============================
   (None = None)

  
  A : Type
  B : Type
  f : A -> option B
  a : A
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  ============================
   (f a = f a)

  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  i : positive
  ============================
   (None = None)

  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  i : positive
  ============================
   (get i (map_filter' f m) = option_map f (get' i m))

  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  ============================
   (None = None)

  
  A : Type
  B : Type
  f : A -> option B
  m1 : tree' A
  m2 : tree' A
  IHm1 : forall i : positive,
         get i (map_filter' f m1) = option_map f (get' i m1)
  IHm2 : forall i : positive,
         get i (map_filter' f m2) = option_map f (get' i m2)
  i : positive
  ============================
   (get i (map_filter' f m2) = option_map f (get' i m2))

  
  A : Type
  B : Type
  f : A -> option B
  m1 : tree' A
  m2 : tree' A
  IHm1 : forall i : positive,
         get i (map_filter' f m1) = option_map f (get' i m1)
  IHm2 : forall i : positive,
         get i (map_filter' f m2) = option_map f (get' i m2)
  i : positive
  ============================
   (get i (map_filter' f m1) = option_map f (get' i m1))

  
  A : Type
  B : Type
  f : A -> option B
  m1 : tree' A
  m2 : tree' A
  IHm1 : forall i : positive,
         get i (map_filter' f m1) = option_map f (get' i m1)
  IHm2 : forall i : positive,
         get i (map_filter' f m2) = option_map f (get' i m2)
  ============================
   (None = None)

  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  a : A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  i : positive
  ============================
   (None = None)

  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  a : A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  i : positive
  ============================
   (get i (map_filter' f m) = option_map f (get' i m))

  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  a : A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  ============================
   (f a = f a)

  
  A : Type
  B : Type
  f : A -> option B
  m1 : tree' A
  a : A
  m2 : tree' A
  IHm1 : forall i : positive,
         get i (map_filter' f m1) = option_map f (get' i m1)
  IHm2 : forall i : positive,
         get i (map_filter' f m2) = option_map f (get' i m2)
  i : positive
  ============================
   (get i (map_filter' f m2) = option_map f (get' i m2))

  
  A : Type
  B : Type
  f : A -> option B
  m1 : tree' A
  a : A
  m2 : tree' A
  IHm1 : forall i : positive,
         get i (map_filter' f m1) = option_map f (get' i m1)
  IHm2 : forall i : positive,
         get i (map_filter' f m2) = option_map f (get' i m2)
  i : positive
  ============================
   (get i (map_filter' f m1) = option_map f (get' i m1))

  
  A : Type
  B : Type
  f : A -> option B
  m1 : tree' A
  a : A
  m2 : tree' A
  IHm1 : forall i : positive,
         get i (map_filter' f m1) = option_map f (get' i m1)
  IHm2 : forall i : positive,
         get i (map_filter' f m2) = option_map f (get' i m2)
  ============================
   (f a = f a)


DEBUG:Going to execute:
auto

Goals:
  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  i : positive
  ============================
   (get i (map_filter' f m) = option_map f (get' i m))

  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  i : positive
  ============================
   (None = None)

  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  ============================
   (None = None)

    A : Type  B : Type  f : A -> option B  a : A  i : positive
  ============================
   (None = None)

    A : Type  B : Type  f : A -> option B  a : A  i : positive
  ============================
   (None = None)

    A : Type  B : Type  f : A -> option B  a : A
  ============================
   (f a = f a)

  
  A : Type
  B : Type
  f : A -> option B
  a : A
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  i : positive
  ============================
   (get i (map_filter' f m) = option_map f (get' i m))

  
  A : Type
  B : Type
  f : A -> option B
  a : A
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  i : positive
  ============================
   (None = None)

  
  A : Type
  B : Type
  f : A -> option B
  a : A
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  ============================
   (f a = f a)

  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  i : positive
  ============================
   (None = None)

  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  i : positive
  ============================
   (get i (map_filter' f m) = option_map f (get' i m))

  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  ============================
   (None = None)

  
  A : Type
  B : Type
  f : A -> option B
  m1 : tree' A
  m2 : tree' A
  IHm1 : forall i : positive,
         get i (map_filter' f m1) = option_map f (get' i m1)
  IHm2 : forall i : positive,
         get i (map_filter' f m2) = option_map f (get' i m2)
  i : positive
  ============================
   (get i (map_filter' f m2) = option_map f (get' i m2))

  
  A : Type
  B : Type
  f : A -> option B
  m1 : tree' A
  m2 : tree' A
  IHm1 : forall i : positive,
         get i (map_filter' f m1) = option_map f (get' i m1)
  IHm2 : forall i : positive,
         get i (map_filter' f m2) = option_map f (get' i m2)
  i : positive
  ============================
   (get i (map_filter' f m1) = option_map f (get' i m1))

  
  A : Type
  B : Type
  f : A -> option B
  m1 : tree' A
  m2 : tree' A
  IHm1 : forall i : positive,
         get i (map_filter' f m1) = option_map f (get' i m1)
  IHm2 : forall i : positive,
         get i (map_filter' f m2) = option_map f (get' i m2)
  ============================
   (None = None)

  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  a : A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  i : positive
  ============================
   (None = None)

  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  a : A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  i : positive
  ============================
   (get i (map_filter' f m) = option_map f (get' i m))

  
  A : Type
  B : Type
  f : A -> option B
  m : tree' A
  a : A
  IHm : forall i : positive,
        get i (map_filter' f m) = option_map f (get' i m)
  ============================
   (f a = f a)

  
  A : Type
  B : Type
  f : A -> option B
  m1 : tree' A
  a : A
  m2 : tree' A
  IHm1 : forall i : positive,
         get i (map_filter' f m1) = option_map f (get' i m1)
  IHm2 : forall i : positive,
         get i (map_filter' f m2) = option_map f (get' i m2)
  i : positive
  ============================
   (get i (map_filter' f m2) = option_map f (get' i m2))

  
  A : Type
  B : Type
  f : A -> option B
  m1 : tree' A
  a : A
  m2 : tree' A
  IHm1 : forall i : positive,
         get i (map_filter' f m1) = option_map f (get' i m1)
  IHm2 : forall i : positive,
         get i (map_filter' f m2) = option_map f (get' i m2)
  i : positive
  ============================
   (get i (map_filter' f m1) = option_map f (get' i m1))

  
  A : Type
  B : Type
  f : A -> option B
  m1 : tree' A
  a : A
  m2 : tree' A
  IHm1 : forall i : positive,
         get i (map_filter' f m1) = option_map f (get' i m1)
  IHm2 : forall i : positive,
         get i (map_filter' f m2) = option_map f (get' i m2)
  ============================
   (f a = f a)


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