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


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