Goal:
    A : Type  i : positive  l : tree A  x : option A  r : tree A
  ============================
   (get i (Node l x r) =
    match i with
    | xI j => get j r
    | xO j => get j l
    | xH => x
    end)


DEBUG:Going to execute:
destruct l, x, r

Goals:
    A : Type  i : positive  a : A
  ============================
   (get i (Node Empty (Some a) Empty) =
    match i with
    | xI j | xO j => get j Empty
    | xH => Some a
    end)

    A : Type  i : positive  a : A  t0 : tree' A
  ============================
   (get i (Node Empty (Some a) (Nodes t0)) =
    match i with
    | xI j => get j (Nodes t0)
    | xO j => get j Empty
    | xH => Some a
    end)

    A : Type  i : positive
  ============================
   (get i (Node Empty None Empty) =
    match i with
    | xI j | xO j => get j Empty
    | xH => None
    end)

    A : Type  i : positive  t0 : tree' A
  ============================
   (get i (Node Empty None (Nodes t0)) =
    match i with
    | xI j => get j (Nodes t0)
    | xO j => get j Empty
    | xH => None
    end)

    A : Type  i : positive  t0 : tree' A  a : A
  ============================
   (get i (Node (Nodes t0) (Some a) Empty) =
    match i with
    | xI j => get j Empty
    | xO j => get j (Nodes t0)
    | xH => Some a
    end)

    A : Type  i : positive  t0 : tree' A  a : A  t1 : tree' A
  ============================
   (get i (Node (Nodes t0) (Some a) (Nodes t1)) =
    match i with
    | xI j => get j (Nodes t1)
    | xO j => get j (Nodes t0)
    | xH => Some a
    end)

    A : Type  i : positive  t0 : tree' A
  ============================
   (get i (Node (Nodes t0) None Empty) =
    match i with
    | xI j => get j Empty
    | xO j => get j (Nodes t0)
    | xH => None
    end)

    A : Type  i : positive  t0 : tree' A  t1 : tree' A
  ============================
   (get i (Node (Nodes t0) None (Nodes t1)) =
    match i with
    | xI j => get j (Nodes t1)
    | xO j => get j (Nodes t0)
    | xH => None
    end)


DEBUG:Going to execute:
simpl
DEBUG LTAC Evaluated term: l
DEBUG LTAC Evaluated term: x
DEBUG LTAC Evaluated term: x
DEBUG LTAC Evaluated term: r
DEBUG LTAC Evaluated term: r
DEBUG LTAC Evaluated term: r
DEBUG LTAC Evaluated term: r

Goals:
    A : Type  i : positive  a : A
  ============================
   (get' i (Node010 a) = match i with
                         | xH => Some a
                         | _ => None
                         end)

    A : Type  i : positive  a : A  t0 : tree' A
  ============================
   (get' i (Node011 a t0) =
    match i with
    | xI j => get' j t0
    | xO _ => None
    | xH => Some a
    end)

    A : Type  i : positive
  ============================
   (None = match i with
           | xI _ | _ => None
           end)

    A : Type  i : positive  t0 : tree' A
  ============================
   (get' i (Node001 t0) = match i with
                          | xI j => get' j t0
                          | _ => None
                          end)

    A : Type  i : positive  t0 : tree' A  a : A
  ============================
   (get' i (Node110 t0 a) =
    match i with
    | xI _ => None
    | xO j => get' j t0
    | xH => Some a
    end)

    A : Type  i : positive  t0 : tree' A  a : A  t1 : tree' A
  ============================
   (get' i (Node111 t0 a t1) =
    match i with
    | xI j => get' j t1
    | xO j => get' j t0
    | xH => Some a
    end)

    A : Type  i : positive  t0 : tree' A
  ============================
   (get' i (Node100 t0) = match i with
                          | xO j => get' j t0
                          | _ => None
                          end)

    A : Type  i : positive  t0 : tree' A  t1 : tree' A
  ============================
   (get' i (Node101 t0 t1) =
    match i with
    | xI j => get' j t1
    | xO j => get' j t0
    | xH => None
    end)


DEBUG:Going to execute:
auto

Goals:
    A : Type  i : positive  a : A
  ============================
   (get' i (Node010 a) = match i with
                         | xH => Some a
                         | _ => None
                         end)

    A : Type  i : positive  a : A  t0 : tree' A
  ============================
   (get' i (Node011 a t0) =
    match i with
    | xI j => get' j t0
    | xO _ => None
    | xH => Some a
    end)

    A : Type  i : positive
  ============================
   (None = match i with
           | xI _ | _ => None
           end)

    A : Type  i : positive  t0 : tree' A
  ============================
   (get' i (Node001 t0) = match i with
                          | xI j => get' j t0
                          | _ => None
                          end)

    A : Type  i : positive  t0 : tree' A  a : A
  ============================
   (get' i (Node110 t0 a) =
    match i with
    | xI _ => None
    | xO j => get' j t0
    | xH => Some a
    end)

    A : Type  i : positive  t0 : tree' A  a : A  t1 : tree' A
  ============================
   (get' i (Node111 t0 a t1) =
    match i with
    | xI j => get' j t1
    | xO j => get' j t0
    | xH => Some a
    end)

    A : Type  i : positive  t0 : tree' A
  ============================
   (get' i (Node100 t0) = match i with
                          | xO j => get' j t0
                          | _ => None
                          end)

    A : Type  i : positive  t0 : tree' A  t1 : tree' A
  ============================
   (get' i (Node101 t0 t1) =
    match i with
    | xI j => get' j t1
    | xO j => get' j t0
    | xH => None
    end)


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

Goals:
    A : Type  i : positive  a : A
  ============================
   (get' i (Node010 a) = match i with
                         | xH => Some a
                         | _ => None
                         end)

    A : Type  i : positive  a : A  t0 : tree' A
  ============================
   (get' i (Node011 a t0) =
    match i with
    | xI j => get' j t0
    | xO _ => None
    | xH => Some a
    end)

    A : Type  i : positive
  ============================
   (None = match i with
           | xI _ | _ => None
           end)

    A : Type  i : positive  t0 : tree' A
  ============================
   (get' i (Node001 t0) = match i with
                          | xI j => get' j t0
                          | _ => None
                          end)

    A : Type  i : positive  t0 : tree' A  a : A
  ============================
   (get' i (Node110 t0 a) =
    match i with
    | xI _ => None
    | xO j => get' j t0
    | xH => Some a
    end)

    A : Type  i : positive  t0 : tree' A  a : A  t1 : tree' A
  ============================
   (get' i (Node111 t0 a t1) =
    match i with
    | xI j => get' j t1
    | xO j => get' j t0
    | xH => Some a
    end)

    A : Type  i : positive  t0 : tree' A
  ============================
   (get' i (Node100 t0) = match i with
                          | xO j => get' j t0
                          | _ => None
                          end)

    A : Type  i : positive  t0 : tree' A  t1 : tree' A
  ============================
   (get' i (Node101 t0 t1) =
    match i with
    | xI j => get' j t1
    | xO j => get' j t0
    | xH => None
    end)


DEBUG:Going to execute:
destruct i

Goals:
    A : Type  i : positive  a : A
  ============================
   (get' (xI i) (Node010 a) = None)

    A : Type  i : positive  a : A
  ============================
   (get' (xO i) (Node010 a) = None)

    A : Type  a : A
  ============================
   (get' xH (Node010 a) = Some a)

    A : Type  i : positive  a : A  t0 : tree' A
  ============================
   (get' (xI i) (Node011 a t0) = get' i t0)

    A : Type  i : positive  a : A  t0 : tree' A
  ============================
   (get' (xO i) (Node011 a t0) = None)

    A : Type  a : A  t0 : tree' A
  ============================
   (get' xH (Node011 a t0) = Some a)

    A : Type  i : positive
  ============================
   (None = None)

    A : Type  i : positive
  ============================
   (None = None)

    A : Type
  ============================
   (None = None)

    A : Type  i : positive  t0 : tree' A
  ============================
   (get' (xI i) (Node001 t0) = get' i t0)

    A : Type  i : positive  t0 : tree' A
  ============================
   (get' (xO i) (Node001 t0) = None)

    A : Type  t0 : tree' A
  ============================
   (get' xH (Node001 t0) = None)

    A : Type  i : positive  t0 : tree' A  a : A
  ============================
   (get' (xI i) (Node110 t0 a) = None)

    A : Type  i : positive  t0 : tree' A  a : A
  ============================
   (get' (xO i) (Node110 t0 a) = get' i t0)

    A : Type  t0 : tree' A  a : A
  ============================
   (get' xH (Node110 t0 a) = Some a)

    A : Type  i : positive  t0 : tree' A  a : A  t1 : tree' A
  ============================
   (get' (xI i) (Node111 t0 a t1) = get' i t1)

    A : Type  i : positive  t0 : tree' A  a : A  t1 : tree' A
  ============================
   (get' (xO i) (Node111 t0 a t1) = get' i t0)

    A : Type  t0 : tree' A  a : A  t1 : tree' A
  ============================
   (get' xH (Node111 t0 a t1) = Some a)

    A : Type  i : positive  t0 : tree' A
  ============================
   (get' (xI i) (Node100 t0) = None)

    A : Type  i : positive  t0 : tree' A
  ============================
   (get' (xO i) (Node100 t0) = get' i t0)

    A : Type  t0 : tree' A
  ============================
   (get' xH (Node100 t0) = None)

    A : Type  i : positive  t0 : tree' A  t1 : tree' A
  ============================
   (get' (xI i) (Node101 t0 t1) = get' i t1)

    A : Type  i : positive  t0 : tree' A  t1 : tree' A
  ============================
   (get' (xO i) (Node101 t0 t1) = get' i t0)

    A : Type  t0 : tree' A  t1 : tree' A
  ============================
   (get' xH (Node101 t0 t1) = None)


DEBUG:Going to execute:
auto
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
DEBUG LTAC Evaluated term: i

Goals:
    A : Type  i : positive  a : A
  ============================
   (get' (xI i) (Node010 a) = None)

    A : Type  i : positive  a : A
  ============================
   (get' (xO i) (Node010 a) = None)

    A : Type  a : A
  ============================
   (get' xH (Node010 a) = Some a)

    A : Type  i : positive  a : A  t0 : tree' A
  ============================
   (get' (xI i) (Node011 a t0) = get' i t0)

    A : Type  i : positive  a : A  t0 : tree' A
  ============================
   (get' (xO i) (Node011 a t0) = None)

    A : Type  a : A  t0 : tree' A
  ============================
   (get' xH (Node011 a t0) = Some a)

    A : Type  i : positive
  ============================
   (None = None)

    A : Type  i : positive
  ============================
   (None = None)

    A : Type
  ============================
   (None = None)

    A : Type  i : positive  t0 : tree' A
  ============================
   (get' (xI i) (Node001 t0) = get' i t0)

    A : Type  i : positive  t0 : tree' A
  ============================
   (get' (xO i) (Node001 t0) = None)

    A : Type  t0 : tree' A
  ============================
   (get' xH (Node001 t0) = None)

    A : Type  i : positive  t0 : tree' A  a : A
  ============================
   (get' (xI i) (Node110 t0 a) = None)

    A : Type  i : positive  t0 : tree' A  a : A
  ============================
   (get' (xO i) (Node110 t0 a) = get' i t0)

    A : Type  t0 : tree' A  a : A
  ============================
   (get' xH (Node110 t0 a) = Some a)

    A : Type  i : positive  t0 : tree' A  a : A  t1 : tree' A
  ============================
   (get' (xI i) (Node111 t0 a t1) = get' i t1)

    A : Type  i : positive  t0 : tree' A  a : A  t1 : tree' A
  ============================
   (get' (xO i) (Node111 t0 a t1) = get' i t0)

    A : Type  t0 : tree' A  a : A  t1 : tree' A
  ============================
   (get' xH (Node111 t0 a t1) = Some a)

    A : Type  i : positive  t0 : tree' A
  ============================
   (get' (xI i) (Node100 t0) = None)

    A : Type  i : positive  t0 : tree' A
  ============================
   (get' (xO i) (Node100 t0) = get' i t0)

    A : Type  t0 : tree' A
  ============================
   (get' xH (Node100 t0) = None)

    A : Type  i : positive  t0 : tree' A  t1 : tree' A
  ============================
   (get' (xI i) (Node101 t0 t1) = get' i t1)

    A : Type  i : positive  t0 : tree' A  t1 : tree' A
  ============================
   (get' (xO i) (Node101 t0 t1) = get' i t0)

    A : Type  t0 : tree' A  t1 : tree' A
  ============================
   (get' xH (Node101 t0 t1) = None)


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