Goal:
    A : Type  x : A
  ============================
   (get xH (set xH x Empty) = Some x)


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