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


DEBUG:Going to execute:
induction p; destruct q; simpl; intros; auto