Goal:
  
  ============================
   (forall (A : Type) (p : positive) (x : A), get' p (set0 p x) = Some x)


DEBUG:Going to execute:
induction p; simpl