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


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

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

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

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


DEBUG:Going to execute:
congruence
Level 0: Backtrace:

The variable IHp was not found in the current environment.

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

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

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


DEBUG:Going to execute:
<coq-core.plugins.cc::cc@0> $1

File "./theories/canonicaltries/CanonicalTries.v", line 216, characters 5-18:
Warning: There is no flag or option with this name: "Debug On".
[unknown-option,default]
File "./theories/canonicaltries/CanonicalTries.v", line 216, characters 5-18:
Warning: There is no flag or option with this name: "Debug On".
[unknown-option,default]