Goal:
    A : Type  i : positive  j : positive  x : A  m : tree A  H : i <> j
  ============================
   (get i (set j x m) = get i m)


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

Goals:
    A : Type  i : positive  j : positive  x : A  H : i <> j
  ============================
   (get i (set j x Empty) = get i Empty)

    A : Type  i : positive  j : positive  x : A  m : tree' A  H : i <> j
  ============================
   (get i (set j x (Nodes m)) = get i (Nodes m))


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