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


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

Goals:
    A : Type  i : positive
  ============================
   (get i (remove i Empty) = None)

    A : Type  i : positive  m : tree' A
  ============================
   (get i (remove i (Nodes m)) = None)


DEBUG:Going to execute:
simpl