Goal:
    A : Type  i : positive
  ============================
   (forall m : tree' A, get i (rem' i m) = None)


DEBUG:Going to execute:
induction i

Goals:
    A : Type  i : positive  IHi : forall m : tree' A, get i (rem' i m) = None
  ============================
   (forall m : tree' A, get (xI i) (rem' (xI i) m) = None)

    A : Type  i : positive  IHi : forall m : tree' A, get i (rem' i m) = None
  ============================
   (forall m : tree' A, get (xO i) (rem' (xO i) m) = None)

    A : Type
  ============================
   (forall m : tree' A, get xH (rem' xH m) = None)


DEBUG:Going to execute:
destruct m
DEBUG LTAC Evaluated term: i

Goals:
  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m : tree' A
  ============================
   (get (xI i) (rem' (xI i) (Node001 m)) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  a : A
  ============================
   (get (xI i) (rem' (xI i) (Node010 a)) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  a : A
  m : tree' A
  ============================
   (get (xI i) (rem' (xI i) (Node011 a m)) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m : tree' A
  ============================
   (get (xI i) (rem' (xI i) (Node100 m)) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m1 : tree' A
  m2 : tree' A
  ============================
   (get (xI i) (rem' (xI i) (Node101 m1 m2)) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m : tree' A
  a : A
  ============================
   (get (xI i) (rem' (xI i) (Node110 m a)) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m1 : tree' A
  a : A
  m2 : tree' A
  ============================
   (get (xI i) (rem' (xI i) (Node111 m1 a m2)) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m : tree' A
  ============================
   (get (xO i) (rem' (xO i) (Node001 m)) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  a : A
  ============================
   (get (xO i) (rem' (xO i) (Node010 a)) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  a : A
  m : tree' A
  ============================
   (get (xO i) (rem' (xO i) (Node011 a m)) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m : tree' A
  ============================
   (get (xO i) (rem' (xO i) (Node100 m)) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m1 : tree' A
  m2 : tree' A
  ============================
   (get (xO i) (rem' (xO i) (Node101 m1 m2)) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m : tree' A
  a : A
  ============================
   (get (xO i) (rem' (xO i) (Node110 m a)) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m1 : tree' A
  a : A
  m2 : tree' A
  ============================
   (get (xO i) (rem' (xO i) (Node111 m1 a m2)) = None)

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

    A : Type  a : A
  ============================
   (get xH (rem' xH (Node010 a)) = None)

    A : Type  a : A  m : tree' A
  ============================
   (get xH (rem' xH (Node011 a m)) = None)

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

    A : Type  m1 : tree' A  m2 : tree' A
  ============================
   (get xH (rem' xH (Node101 m1 m2)) = None)

    A : Type  m : tree' A  a : A
  ============================
   (get xH (rem' xH (Node110 m a)) = None)

    A : Type  m1 : tree' A  a : A  m2 : tree' A
  ============================
   (get xH (rem' xH (Node111 m1 a m2)) = None)


DEBUG:Going to execute:
simpl

Goals:
  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m : tree' A
  ============================
   (get (xI i) (Node Empty None (rem' i m)) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  a : A
  ============================
   (None = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  a : A
  m : tree' A
  ============================
   (get (xI i) (Node Empty (Some a) (rem' i m)) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m : tree' A
  ============================
   (None = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m1 : tree' A
  m2 : tree' A
  ============================
   (get (xI i) (Node (Nodes m1) None (rem' i m2)) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m : tree' A
  a : A
  ============================
   (None = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m1 : tree' A
  a : A
  m2 : tree' A
  ============================
   (get (xI i) (Node (Nodes m1) (Some a) (rem' i m2)) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m : tree' A
  ============================
   (None = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  a : A
  ============================
   (None = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  a : A
  m : tree' A
  ============================
   (None = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m : tree' A
  ============================
   (get (xO i) (Node (rem' i m) None Empty) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m1 : tree' A
  m2 : tree' A
  ============================
   (get (xO i) (Node (rem' i m1) None (Nodes m2)) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m : tree' A
  a : A
  ============================
   (get (xO i) (Node (rem' i m) (Some a) Empty) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m1 : tree' A
  a : A
  m2 : tree' A
  ============================
   (get (xO i) (Node (rem' i m1) (Some a) (Nodes m2)) = None)

    A : Type  m : tree' A
  ============================
   (None = None)

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

    A : Type  a : A  m : tree' A
  ============================
   (None = None)

    A : Type  m : tree' A
  ============================
   (None = None)

    A : Type  m1 : tree' A  m2 : tree' A
  ============================
   (None = None)

    A : Type  m : tree' A  a : A
  ============================
   (None = None)

    A : Type  m1 : tree' A  a : A  m2 : tree' A
  ============================
   (None = None)


DEBUG:Going to execute:
auto

Goals:
  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m : tree' A
  ============================
   (get (xI i) (Node Empty None (rem' i m)) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  a : A
  ============================
   (None = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  a : A
  m : tree' A
  ============================
   (get (xI i) (Node Empty (Some a) (rem' i m)) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m : tree' A
  ============================
   (None = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m1 : tree' A
  m2 : tree' A
  ============================
   (get (xI i) (Node (Nodes m1) None (rem' i m2)) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m : tree' A
  a : A
  ============================
   (None = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m1 : tree' A
  a : A
  m2 : tree' A
  ============================
   (get (xI i) (Node (Nodes m1) (Some a) (rem' i m2)) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m : tree' A
  ============================
   (None = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  a : A
  ============================
   (None = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  a : A
  m : tree' A
  ============================
   (None = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m : tree' A
  ============================
   (get (xO i) (Node (rem' i m) None Empty) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m1 : tree' A
  m2 : tree' A
  ============================
   (get (xO i) (Node (rem' i m1) None (Nodes m2)) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m : tree' A
  a : A
  ============================
   (get (xO i) (Node (rem' i m) (Some a) Empty) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m1 : tree' A
  a : A
  m2 : tree' A
  ============================
   (get (xO i) (Node (rem' i m1) (Some a) (Nodes m2)) = None)

    A : Type  m : tree' A
  ============================
   (None = None)

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

    A : Type  a : A  m : tree' A
  ============================
   (None = None)

    A : Type  m : tree' A
  ============================
   (None = None)

    A : Type  m1 : tree' A  m2 : tree' A
  ============================
   (None = None)

    A : Type  m : tree' A  a : A
  ============================
   (None = None)

    A : Type  m1 : tree' A  a : A  m2 : tree' A
  ============================
   (None = None)


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

Goals:
  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m : tree' A
  ============================
   (get (xI i) (Node Empty None (rem' i m)) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  a : A
  m : tree' A
  ============================
   (get (xI i) (Node Empty (Some a) (rem' i m)) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m1 : tree' A
  m2 : tree' A
  ============================
   (get (xI i) (Node (Nodes m1) None (rem' i m2)) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m1 : tree' A
  a : A
  m2 : tree' A
  ============================
   (get (xI i) (Node (Nodes m1) (Some a) (rem' i m2)) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m : tree' A
  ============================
   (get (xO i) (Node (rem' i m) None Empty) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m1 : tree' A
  m2 : tree' A
  ============================
   (get (xO i) (Node (rem' i m1) None (Nodes m2)) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m : tree' A
  a : A
  ============================
   (get (xO i) (Node (rem' i m) (Some a) Empty) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m1 : tree' A
  a : A
  m2 : tree' A
  ============================
   (get (xO i) (Node (rem' i m1) (Some a) (Nodes m2)) = None)


DEBUG:Going to execute:
rewrite gNode

Goals:
  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m : tree' A
  ============================
   (get i (rem' i m) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  a : A
  m : tree' A
  ============================
   (get i (rem' i m) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m1 : tree' A
  m2 : tree' A
  ============================
   (get i (rem' i m2) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m1 : tree' A
  a : A
  m2 : tree' A
  ============================
   (get i (rem' i m2) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m : tree' A
  ============================
   (get i (rem' i m) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m1 : tree' A
  m2 : tree' A
  ============================
   (get i (rem' i m1) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m : tree' A
  a : A
  ============================
   (get i (rem' i m) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m1 : tree' A
  a : A
  m2 : tree' A
  ============================
   (get i (rem' i m1) = None)


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

Goals:
  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m : tree' A
  ============================
   (get i (rem' i m) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  a : A
  m : tree' A
  ============================
   (get i (rem' i m) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m1 : tree' A
  m2 : tree' A
  ============================
   (get i (rem' i m2) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m1 : tree' A
  a : A
  m2 : tree' A
  ============================
   (get i (rem' i m2) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m : tree' A
  ============================
   (get i (rem' i m) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m1 : tree' A
  m2 : tree' A
  ============================
   (get i (rem' i m1) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m : tree' A
  a : A
  ============================
   (get i (rem' i m) = None)

  
  A : Type
  i : positive
  IHi : forall m : tree' A, get i (rem' i m) = None
  m1 : tree' A
  a : A
  m2 : tree' A
  ============================
   (get i (rem' i m1) = None)


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