Goal:
    A : Type  j : positive  x : A  H : xH <> xO j
  ============================
   (get xH (set (xO j) x Empty) = get xH Empty)


DEBUG:Going to execute:
rewrite set_Empty
DEBUG LTAC Evaluated term: set_Node
DEBUG LTAC Evaluated term: set_Node