Goal:
  
  A : Type
  p : positive
  IHp : forall (q : positive) (x : A), p <> q -> get' p (set0 q x) = None
  q : positive
  x : A
  H : xO p <> xO q
  ============================
   (get' p (set0 q x) = None)


DEBUG:Going to execute:
apply IHp
DEBUG LTAC Evaluated term: IHp