Goal:
    A : Type  m : tree A  H : forall i : positive, get i m = None
  ============================
   (m = Empty)


DEBUG:Going to execute:
destruct m as [| m]

Goals:
    A : Type  H : forall i : positive, get i Empty = None
  ============================
   (Empty = Empty)

    A : Type  m : tree' A  H : forall i : positive, get i (Nodes m) = None
  ============================
   (Nodes m = Empty)


DEBUG:Going to execute:
auto
DEBUG LTAC Evaluated term: m

Goals:
    A : Type  H : forall i : positive, get i Empty = None
  ============================
   (Empty = Empty)

    A : Type  m : tree' A  H : forall i : positive, get i (Nodes m) = None
  ============================
   (Nodes m = Empty)


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