Goal:
    A : Type  i : positive  x : A  m : tree A
  ============================
   (get i (set i x m) = Some x)


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

Goals:
    A : Type  i : positive  x : A
  ============================
   (get i (set i x Empty) = Some x)

    A : Type  i : positive  x : A  m : tree' A
  ============================
   (get i (set i x (Nodes m)) = Some x)


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