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


DEBUG:Going to execute:
induction p

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

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

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


DEBUG:Going to execute:
destruct q

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

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

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

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

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

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

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

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

    A : Type
  ============================
   (forall x : A, xH <> xH -> get' xH (set0 xH x) = None)


DEBUG:Going to execute:
simpl

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

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

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

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

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

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

    A : Type  q : positive
  ============================
   (A -> xH <> xI q -> None = None)

    A : Type  q : positive
  ============================
   (A -> xH <> xO q -> None = None)

    A : Type
  ============================
   (forall x : A, xH <> xH -> Some x = None)


DEBUG:Going to execute:
intros

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

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

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

  
  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 <> xI q
  ============================
   (None = None)

  
  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)

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

    A : Type  q : positive  x : A  H : xH <> xI q
  ============================
   (None = None)

    A : Type  q : positive  x : A  H : xH <> xO q
  ============================
   (None = None)

    A : Type  x : A  H : xH <> xH
  ============================
   (Some x = None)


DEBUG:Going to execute:
auto

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

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

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

  
  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 <> xI q
  ============================
   (None = None)

  
  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)

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

    A : Type  q : positive  x : A  H : xH <> xI q
  ============================
   (None = None)

    A : Type  q : positive  x : A  H : xH <> xO q
  ============================
   (None = None)

    A : Type  x : A  H : xH <> xH
  ============================
   (Some x = None)


DEBUG:Going to execute:
<coq-core.plugins.ltac::auto@0> $1 $2 $3

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

  
  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)

    A : Type  x : A  H : xH <> xH
  ============================
   (Some x = None)


DEBUG:Going to execute:
try apply IHp