Goal:
  
  ============================
   (forall (A : Type) (i j : positive) (m : tree A),
    i <> j -> get i (remove j m) = get i m)


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

Goals:
    A : Type  i : positive  j : positive
  ============================
   (i <> j -> get i (remove j Empty) = get i Empty)

    A : Type  i : positive  j : positive  m : tree' A
  ============================
   (i <> j -> get i (remove j (Nodes m)) = get i (Nodes m))


DEBUG:Going to execute:
simpl