Goal:
    A : Type  i : positive  x : A
  ============================
   (forall (m : tree' A) (j : positive),
    i <> j -> get' i (set' j x m) = get' i m)


DEBUG:Going to execute:
induction i

Goals:
  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  ============================
   (forall (m : tree' A) (j : positive),
    xI i <> j -> get' (xI i) (set' j x m) = get' (xI i) m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  ============================
   (forall (m : tree' A) (j : positive),
    xO i <> j -> get' (xO i) (set' j x m) = get' (xO i) m)

    A : Type  x : A
  ============================
   (forall (m : tree' A) (j : positive),
    xH <> j -> get' xH (set' j x m) = get' xH m)


DEBUG:Going to execute:
destruct j, m
DEBUG LTAC Evaluated term: i

Goals:
  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  ============================
   (xI i <> xI j ->
    get' (xI i) (set' (xI j) x (Node001 m)) = get' (xI i) (Node001 m))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  j : positive
  ============================
   (xI i <> xI j ->
    get' (xI i) (set' (xI j) x (Node010 a)) = get' (xI i) (Node010 a))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  m : tree' A
  j : positive
  ============================
   (xI i <> xI j ->
    get' (xI i) (set' (xI j) x (Node011 a m)) = get' (xI i) (Node011 a m))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  ============================
   (xI i <> xI j ->
    get' (xI i) (set' (xI j) x (Node100 m)) = get' (xI i) (Node100 m))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  m2 : tree' A
  j : positive
  ============================
   (xI i <> xI j ->
    get' (xI i) (set' (xI j) x (Node101 m1 m2)) = get' (xI i) (Node101 m1 m2))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  a : A
  j : positive
  ============================
   (xI i <> xI j ->
    get' (xI i) (set' (xI j) x (Node110 m a)) = get' (xI i) (Node110 m a))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  a : A
  m2 : tree' A
  j : positive
  ============================
   (xI i <> xI j ->
    get' (xI i) (set' (xI j) x (Node111 m1 a m2)) =
    get' (xI i) (Node111 m1 a m2))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  ============================
   (xI i <> xO j ->
    get' (xI i) (set' (xO j) x (Node001 m)) = get' (xI i) (Node001 m))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  j : positive
  ============================
   (xI i <> xO j ->
    get' (xI i) (set' (xO j) x (Node010 a)) = get' (xI i) (Node010 a))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  m : tree' A
  j : positive
  ============================
   (xI i <> xO j ->
    get' (xI i) (set' (xO j) x (Node011 a m)) = get' (xI i) (Node011 a m))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  ============================
   (xI i <> xO j ->
    get' (xI i) (set' (xO j) x (Node100 m)) = get' (xI i) (Node100 m))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  m2 : tree' A
  j : positive
  ============================
   (xI i <> xO j ->
    get' (xI i) (set' (xO j) x (Node101 m1 m2)) = get' (xI i) (Node101 m1 m2))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  a : A
  j : positive
  ============================
   (xI i <> xO j ->
    get' (xI i) (set' (xO j) x (Node110 m a)) = get' (xI i) (Node110 m a))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  a : A
  m2 : tree' A
  j : positive
  ============================
   (xI i <> xO j ->
    get' (xI i) (set' (xO j) x (Node111 m1 a m2)) =
    get' (xI i) (Node111 m1 a m2))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  ============================
   (xI i <> xH ->
    get' (xI i) (set' xH x (Node001 m)) = get' (xI i) (Node001 m))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  ============================
   (xI i <> xH ->
    get' (xI i) (set' xH x (Node010 a)) = get' (xI i) (Node010 a))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  m : tree' A
  ============================
   (xI i <> xH ->
    get' (xI i) (set' xH x (Node011 a m)) = get' (xI i) (Node011 a m))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  ============================
   (xI i <> xH ->
    get' (xI i) (set' xH x (Node100 m)) = get' (xI i) (Node100 m))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  m2 : tree' A
  ============================
   (xI i <> xH ->
    get' (xI i) (set' xH x (Node101 m1 m2)) = get' (xI i) (Node101 m1 m2))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  a : A
  ============================
   (xI i <> xH ->
    get' (xI i) (set' xH x (Node110 m a)) = get' (xI i) (Node110 m a))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  a : A
  m2 : tree' A
  ============================
   (xI i <> xH ->
    get' (xI i) (set' xH x (Node111 m1 a m2)) = get' (xI i) (Node111 m1 a m2))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  ============================
   (xO i <> xI j ->
    get' (xO i) (set' (xI j) x (Node001 m)) = get' (xO i) (Node001 m))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  j : positive
  ============================
   (xO i <> xI j ->
    get' (xO i) (set' (xI j) x (Node010 a)) = get' (xO i) (Node010 a))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  m : tree' A
  j : positive
  ============================
   (xO i <> xI j ->
    get' (xO i) (set' (xI j) x (Node011 a m)) = get' (xO i) (Node011 a m))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  ============================
   (xO i <> xI j ->
    get' (xO i) (set' (xI j) x (Node100 m)) = get' (xO i) (Node100 m))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  m2 : tree' A
  j : positive
  ============================
   (xO i <> xI j ->
    get' (xO i) (set' (xI j) x (Node101 m1 m2)) = get' (xO i) (Node101 m1 m2))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  a : A
  j : positive
  ============================
   (xO i <> xI j ->
    get' (xO i) (set' (xI j) x (Node110 m a)) = get' (xO i) (Node110 m a))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  a : A
  m2 : tree' A
  j : positive
  ============================
   (xO i <> xI j ->
    get' (xO i) (set' (xI j) x (Node111 m1 a m2)) =
    get' (xO i) (Node111 m1 a m2))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  ============================
   (xO i <> xO j ->
    get' (xO i) (set' (xO j) x (Node001 m)) = get' (xO i) (Node001 m))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  j : positive
  ============================
   (xO i <> xO j ->
    get' (xO i) (set' (xO j) x (Node010 a)) = get' (xO i) (Node010 a))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  m : tree' A
  j : positive
  ============================
   (xO i <> xO j ->
    get' (xO i) (set' (xO j) x (Node011 a m)) = get' (xO i) (Node011 a m))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  ============================
   (xO i <> xO j ->
    get' (xO i) (set' (xO j) x (Node100 m)) = get' (xO i) (Node100 m))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  m2 : tree' A
  j : positive
  ============================
   (xO i <> xO j ->
    get' (xO i) (set' (xO j) x (Node101 m1 m2)) = get' (xO i) (Node101 m1 m2))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  a : A
  j : positive
  ============================
   (xO i <> xO j ->
    get' (xO i) (set' (xO j) x (Node110 m a)) = get' (xO i) (Node110 m a))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  a : A
  m2 : tree' A
  j : positive
  ============================
   (xO i <> xO j ->
    get' (xO i) (set' (xO j) x (Node111 m1 a m2)) =
    get' (xO i) (Node111 m1 a m2))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  ============================
   (xO i <> xH ->
    get' (xO i) (set' xH x (Node001 m)) = get' (xO i) (Node001 m))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  ============================
   (xO i <> xH ->
    get' (xO i) (set' xH x (Node010 a)) = get' (xO i) (Node010 a))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  m : tree' A
  ============================
   (xO i <> xH ->
    get' (xO i) (set' xH x (Node011 a m)) = get' (xO i) (Node011 a m))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  ============================
   (xO i <> xH ->
    get' (xO i) (set' xH x (Node100 m)) = get' (xO i) (Node100 m))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  m2 : tree' A
  ============================
   (xO i <> xH ->
    get' (xO i) (set' xH x (Node101 m1 m2)) = get' (xO i) (Node101 m1 m2))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  a : A
  ============================
   (xO i <> xH ->
    get' (xO i) (set' xH x (Node110 m a)) = get' (xO i) (Node110 m a))

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  a : A
  m2 : tree' A
  ============================
   (xO i <> xH ->
    get' (xO i) (set' xH x (Node111 m1 a m2)) = get' (xO i) (Node111 m1 a m2))

    A : Type  x : A  m : tree' A  j : positive
  ============================
   (xH <> xI j -> get' xH (set' (xI j) x (Node001 m)) = get' xH (Node001 m))

    A : Type  x : A  a : A  j : positive
  ============================
   (xH <> xI j -> get' xH (set' (xI j) x (Node010 a)) = get' xH (Node010 a))

    A : Type  x : A  a : A  m : tree' A  j : positive
  ============================
   (xH <> xI j ->
    get' xH (set' (xI j) x (Node011 a m)) = get' xH (Node011 a m))

    A : Type  x : A  m : tree' A  j : positive
  ============================
   (xH <> xI j -> get' xH (set' (xI j) x (Node100 m)) = get' xH (Node100 m))

    A : Type  x : A  m1 : tree' A  m2 : tree' A  j : positive
  ============================
   (xH <> xI j ->
    get' xH (set' (xI j) x (Node101 m1 m2)) = get' xH (Node101 m1 m2))

    A : Type  x : A  m : tree' A  a : A  j : positive
  ============================
   (xH <> xI j ->
    get' xH (set' (xI j) x (Node110 m a)) = get' xH (Node110 m a))

    A : Type  x : A  m1 : tree' A  a : A  m2 : tree' A  j : positive
  ============================
   (xH <> xI j ->
    get' xH (set' (xI j) x (Node111 m1 a m2)) = get' xH (Node111 m1 a m2))

    A : Type  x : A  m : tree' A  j : positive
  ============================
   (xH <> xO j -> get' xH (set' (xO j) x (Node001 m)) = get' xH (Node001 m))

    A : Type  x : A  a : A  j : positive
  ============================
   (xH <> xO j -> get' xH (set' (xO j) x (Node010 a)) = get' xH (Node010 a))

    A : Type  x : A  a : A  m : tree' A  j : positive
  ============================
   (xH <> xO j ->
    get' xH (set' (xO j) x (Node011 a m)) = get' xH (Node011 a m))

    A : Type  x : A  m : tree' A  j : positive
  ============================
   (xH <> xO j -> get' xH (set' (xO j) x (Node100 m)) = get' xH (Node100 m))

    A : Type  x : A  m1 : tree' A  m2 : tree' A  j : positive
  ============================
   (xH <> xO j ->
    get' xH (set' (xO j) x (Node101 m1 m2)) = get' xH (Node101 m1 m2))

    A : Type  x : A  m : tree' A  a : A  j : positive
  ============================
   (xH <> xO j ->
    get' xH (set' (xO j) x (Node110 m a)) = get' xH (Node110 m a))

    A : Type  x : A  m1 : tree' A  a : A  m2 : tree' A  j : positive
  ============================
   (xH <> xO j ->
    get' xH (set' (xO j) x (Node111 m1 a m2)) = get' xH (Node111 m1 a m2))

    A : Type  x : A  m : tree' A
  ============================
   (xH <> xH -> get' xH (set' xH x (Node001 m)) = get' xH (Node001 m))

    A : Type  x : A  a : A
  ============================
   (xH <> xH -> get' xH (set' xH x (Node010 a)) = get' xH (Node010 a))

    A : Type  x : A  a : A  m : tree' A
  ============================
   (xH <> xH -> get' xH (set' xH x (Node011 a m)) = get' xH (Node011 a m))

    A : Type  x : A  m : tree' A
  ============================
   (xH <> xH -> get' xH (set' xH x (Node100 m)) = get' xH (Node100 m))

    A : Type  x : A  m1 : tree' A  m2 : tree' A
  ============================
   (xH <> xH -> get' xH (set' xH x (Node101 m1 m2)) = get' xH (Node101 m1 m2))

    A : Type  x : A  m : tree' A  a : A
  ============================
   (xH <> xH -> get' xH (set' xH x (Node110 m a)) = get' xH (Node110 m a))

    A : Type  x : A  m1 : tree' A  a : A  m2 : tree' A
  ============================
   (xH <> xH ->
    get' xH (set' xH x (Node111 m1 a m2)) = get' xH (Node111 m1 a m2))


DEBUG:Going to execute:
simpl

Goals:
  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  ============================
   (xI i <> xI j -> get' i (set' j x m) = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  j : positive
  ============================
   (xI i <> xI j -> get' i (set0 j x) = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  m : tree' A
  j : positive
  ============================
   (xI i <> xI j -> get' i (set' j x m) = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  ============================
   (xI i <> xI j -> get' i (set0 j x) = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  m2 : tree' A
  j : positive
  ============================
   (xI i <> xI j -> get' i (set' j x m2) = get' i m2)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  a : A
  j : positive
  ============================
   (xI i <> xI j -> get' i (set0 j x) = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  a : A
  m2 : tree' A
  j : positive
  ============================
   (xI i <> xI j -> get' i (set' j x m2) = get' i m2)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  ============================
   (xI i <> xO j -> get' i m = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  j : positive
  ============================
   (xI i <> xO j -> None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  m : tree' A
  j : positive
  ============================
   (xI i <> xO j -> get' i m = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  ============================
   (xI i <> xO j -> None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  m2 : tree' A
  j : positive
  ============================
   (xI i <> xO j -> get' i m2 = get' i m2)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  a : A
  j : positive
  ============================
   (xI i <> xO j -> None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  a : A
  m2 : tree' A
  j : positive
  ============================
   (xI i <> xO j -> get' i m2 = get' i m2)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  ============================
   (xI i <> xH -> get' i m = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  ============================
   (xI i <> xH -> None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  m : tree' A
  ============================
   (xI i <> xH -> get' i m = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  ============================
   (xI i <> xH -> None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  m2 : tree' A
  ============================
   (xI i <> xH -> get' i m2 = get' i m2)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  a : A
  ============================
   (xI i <> xH -> None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  a : A
  m2 : tree' A
  ============================
   (xI i <> xH -> get' i m2 = get' i m2)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  ============================
   (xO i <> xI j -> None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  j : positive
  ============================
   (xO i <> xI j -> None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  m : tree' A
  j : positive
  ============================
   (xO i <> xI j -> None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  ============================
   (xO i <> xI j -> get' i m = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  m2 : tree' A
  j : positive
  ============================
   (xO i <> xI j -> get' i m1 = get' i m1)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  a : A
  j : positive
  ============================
   (xO i <> xI j -> get' i m = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  a : A
  m2 : tree' A
  j : positive
  ============================
   (xO i <> xI j -> get' i m1 = get' i m1)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  ============================
   (xO i <> xO j -> get' i (set0 j x) = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  j : positive
  ============================
   (xO i <> xO j -> get' i (set0 j x) = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  m : tree' A
  j : positive
  ============================
   (xO i <> xO j -> get' i (set0 j x) = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  ============================
   (xO i <> xO j -> get' i (set' j x m) = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  m2 : tree' A
  j : positive
  ============================
   (xO i <> xO j -> get' i (set' j x m1) = get' i m1)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  a : A
  j : positive
  ============================
   (xO i <> xO j -> get' i (set' j x m) = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  a : A
  m2 : tree' A
  j : positive
  ============================
   (xO i <> xO j -> get' i (set' j x m1) = get' i m1)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  ============================
   (xO i <> xH -> None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  ============================
   (xO i <> xH -> None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  m : tree' A
  ============================
   (xO i <> xH -> None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  ============================
   (xO i <> xH -> get' i m = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  m2 : tree' A
  ============================
   (xO i <> xH -> get' i m1 = get' i m1)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  a : A
  ============================
   (xO i <> xH -> get' i m = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  a : A
  m2 : tree' A
  ============================
   (xO i <> xH -> get' i m1 = get' i m1)

    A : Type  x : A  m : tree' A  j : positive
  ============================
   (xH <> xI j -> None = None)

    A : Type  x : A  a : A  j : positive
  ============================
   (xH <> xI j -> Some a = Some a)

    A : Type  x : A  a : A  m : tree' A  j : positive
  ============================
   (xH <> xI j -> Some a = Some a)

    A : Type  x : A  m : tree' A  j : positive
  ============================
   (xH <> xI j -> None = None)

    A : Type  x : A  m1 : tree' A  m2 : tree' A  j : positive
  ============================
   (xH <> xI j -> None = None)

    A : Type  x : A  m : tree' A  a : A  j : positive
  ============================
   (xH <> xI j -> Some a = Some a)

    A : Type  x : A  m1 : tree' A  a : A  m2 : tree' A  j : positive
  ============================
   (xH <> xI j -> Some a = Some a)

    A : Type  x : A  m : tree' A  j : positive
  ============================
   (xH <> xO j -> None = None)

    A : Type  x : A  a : A  j : positive
  ============================
   (xH <> xO j -> Some a = Some a)

    A : Type  x : A  a : A  m : tree' A  j : positive
  ============================
   (xH <> xO j -> Some a = Some a)

    A : Type  x : A  m : tree' A  j : positive
  ============================
   (xH <> xO j -> None = None)

    A : Type  x : A  m1 : tree' A  m2 : tree' A  j : positive
  ============================
   (xH <> xO j -> None = None)

    A : Type  x : A  m : tree' A  a : A  j : positive
  ============================
   (xH <> xO j -> Some a = Some a)

    A : Type  x : A  m1 : tree' A  a : A  m2 : tree' A  j : positive
  ============================
   (xH <> xO j -> Some a = Some a)

    A : Type  x : A  m : tree' A
  ============================
   (xH <> xH -> Some x = None)

    A : Type  x : A  a : A
  ============================
   (xH <> xH -> Some x = Some a)

    A : Type  x : A  a : A  m : tree' A
  ============================
   (xH <> xH -> Some x = Some a)

    A : Type  x : A  m : tree' A
  ============================
   (xH <> xH -> Some x = None)

    A : Type  x : A  m1 : tree' A  m2 : tree' A
  ============================
   (xH <> xH -> Some x = None)

    A : Type  x : A  m : tree' A  a : A
  ============================
   (xH <> xH -> Some x = Some a)

    A : Type  x : A  m1 : tree' A  a : A  m2 : tree' A
  ============================
   (xH <> xH -> Some x = Some a)


DEBUG:Going to execute:
intros

Goals:
  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  H : xI i <> xI j
  ============================
   (get' i (set' j x m) = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  j : positive
  H : xI i <> xI j
  ============================
   (get' i (set0 j x) = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  m : tree' A
  j : positive
  H : xI i <> xI j
  ============================
   (get' i (set' j x m) = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  H : xI i <> xI j
  ============================
   (get' i (set0 j x) = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  m2 : tree' A
  j : positive
  H : xI i <> xI j
  ============================
   (get' i (set' j x m2) = get' i m2)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  a : A
  j : positive
  H : xI i <> xI j
  ============================
   (get' i (set0 j x) = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  a : A
  m2 : tree' A
  j : positive
  H : xI i <> xI j
  ============================
   (get' i (set' j x m2) = get' i m2)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  H : xI i <> xO j
  ============================
   (get' i m = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  j : positive
  H : xI i <> xO j
  ============================
   (None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  m : tree' A
  j : positive
  H : xI i <> xO j
  ============================
   (get' i m = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  H : xI i <> xO j
  ============================
   (None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  m2 : tree' A
  j : positive
  H : xI i <> xO j
  ============================
   (get' i m2 = get' i m2)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  a : A
  j : positive
  H : xI i <> xO j
  ============================
   (None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  a : A
  m2 : tree' A
  j : positive
  H : xI i <> xO j
  ============================
   (get' i m2 = get' i m2)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  H : xI i <> xH
  ============================
   (get' i m = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  H : xI i <> xH
  ============================
   (None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  m : tree' A
  H : xI i <> xH
  ============================
   (get' i m = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  H : xI i <> xH
  ============================
   (None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  m2 : tree' A
  H : xI i <> xH
  ============================
   (get' i m2 = get' i m2)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  a : A
  H : xI i <> xH
  ============================
   (None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  a : A
  m2 : tree' A
  H : xI i <> xH
  ============================
   (get' i m2 = get' i m2)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  H : xO i <> xI j
  ============================
   (None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  j : positive
  H : xO i <> xI j
  ============================
   (None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  m : tree' A
  j : positive
  H : xO i <> xI j
  ============================
   (None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  H : xO i <> xI j
  ============================
   (get' i m = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  m2 : tree' A
  j : positive
  H : xO i <> xI j
  ============================
   (get' i m1 = get' i m1)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  a : A
  j : positive
  H : xO i <> xI j
  ============================
   (get' i m = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  a : A
  m2 : tree' A
  j : positive
  H : xO i <> xI j
  ============================
   (get' i m1 = get' i m1)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  H : xO i <> xO j
  ============================
   (get' i (set0 j x) = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  j : positive
  H : xO i <> xO j
  ============================
   (get' i (set0 j x) = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  m : tree' A
  j : positive
  H : xO i <> xO j
  ============================
   (get' i (set0 j x) = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  H : xO i <> xO j
  ============================
   (get' i (set' j x m) = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  m2 : tree' A
  j : positive
  H : xO i <> xO j
  ============================
   (get' i (set' j x m1) = get' i m1)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  a : A
  j : positive
  H : xO i <> xO j
  ============================
   (get' i (set' j x m) = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  a : A
  m2 : tree' A
  j : positive
  H : xO i <> xO j
  ============================
   (get' i (set' j x m1) = get' i m1)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  H : xO i <> xH
  ============================
   (None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  H : xO i <> xH
  ============================
   (None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  m : tree' A
  H : xO i <> xH
  ============================
   (None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  H : xO i <> xH
  ============================
   (get' i m = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  m2 : tree' A
  H : xO i <> xH
  ============================
   (get' i m1 = get' i m1)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  a : A
  H : xO i <> xH
  ============================
   (get' i m = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  a : A
  m2 : tree' A
  H : xO i <> xH
  ============================
   (get' i m1 = get' i m1)

    A : Type  x : A  m : tree' A  j : positive  H : xH <> xI j
  ============================
   (None = None)

    A : Type  x : A  a : A  j : positive  H : xH <> xI j
  ============================
   (Some a = Some a)

    A : Type  x : A  a : A  m : tree' A  j : positive  H : xH <> xI j
  ============================
   (Some a = Some a)

    A : Type  x : A  m : tree' A  j : positive  H : xH <> xI j
  ============================
   (None = None)

    A : Type  x : A  m1 : tree' A  m2 : tree' A  j : positive  H : xH <> xI j
  ============================
   (None = None)

    A : Type  x : A  m : tree' A  a : A  j : positive  H : xH <> xI j
  ============================
   (Some a = Some a)

  
  A : Type
  x : A
  m1 : tree' A
  a : A
  m2 : tree' A
  j : positive
  H : xH <> xI j
  ============================
   (Some a = Some a)

    A : Type  x : A  m : tree' A  j : positive  H : xH <> xO j
  ============================
   (None = None)

    A : Type  x : A  a : A  j : positive  H : xH <> xO j
  ============================
   (Some a = Some a)

    A : Type  x : A  a : A  m : tree' A  j : positive  H : xH <> xO j
  ============================
   (Some a = Some a)

    A : Type  x : A  m : tree' A  j : positive  H : xH <> xO j
  ============================
   (None = None)

    A : Type  x : A  m1 : tree' A  m2 : tree' A  j : positive  H : xH <> xO j
  ============================
   (None = None)

    A : Type  x : A  m : tree' A  a : A  j : positive  H : xH <> xO j
  ============================
   (Some a = Some a)

  
  A : Type
  x : A
  m1 : tree' A
  a : A
  m2 : tree' A
  j : positive
  H : xH <> xO j
  ============================
   (Some a = Some a)

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

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

    A : Type  x : A  a : A  m : tree' A  H : xH <> xH
  ============================
   (Some x = Some a)

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

    A : Type  x : A  m1 : tree' A  m2 : tree' A  H : xH <> xH
  ============================
   (Some x = None)

    A : Type  x : A  m : tree' A  a : A  H : xH <> xH
  ============================
   (Some x = Some a)

    A : Type  x : A  m1 : tree' A  a : A  m2 : tree' A  H : xH <> xH
  ============================
   (Some x = Some a)


DEBUG:Going to execute:
auto

Goals:
  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  H : xI i <> xI j
  ============================
   (get' i (set' j x m) = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  j : positive
  H : xI i <> xI j
  ============================
   (get' i (set0 j x) = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  m : tree' A
  j : positive
  H : xI i <> xI j
  ============================
   (get' i (set' j x m) = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  H : xI i <> xI j
  ============================
   (get' i (set0 j x) = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  m2 : tree' A
  j : positive
  H : xI i <> xI j
  ============================
   (get' i (set' j x m2) = get' i m2)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  a : A
  j : positive
  H : xI i <> xI j
  ============================
   (get' i (set0 j x) = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  a : A
  m2 : tree' A
  j : positive
  H : xI i <> xI j
  ============================
   (get' i (set' j x m2) = get' i m2)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  H : xI i <> xO j
  ============================
   (get' i m = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  j : positive
  H : xI i <> xO j
  ============================
   (None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  m : tree' A
  j : positive
  H : xI i <> xO j
  ============================
   (get' i m = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  H : xI i <> xO j
  ============================
   (None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  m2 : tree' A
  j : positive
  H : xI i <> xO j
  ============================
   (get' i m2 = get' i m2)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  a : A
  j : positive
  H : xI i <> xO j
  ============================
   (None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  a : A
  m2 : tree' A
  j : positive
  H : xI i <> xO j
  ============================
   (get' i m2 = get' i m2)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  H : xI i <> xH
  ============================
   (get' i m = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  H : xI i <> xH
  ============================
   (None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  m : tree' A
  H : xI i <> xH
  ============================
   (get' i m = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  H : xI i <> xH
  ============================
   (None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  m2 : tree' A
  H : xI i <> xH
  ============================
   (get' i m2 = get' i m2)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  a : A
  H : xI i <> xH
  ============================
   (None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  a : A
  m2 : tree' A
  H : xI i <> xH
  ============================
   (get' i m2 = get' i m2)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  H : xO i <> xI j
  ============================
   (None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  j : positive
  H : xO i <> xI j
  ============================
   (None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  m : tree' A
  j : positive
  H : xO i <> xI j
  ============================
   (None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  H : xO i <> xI j
  ============================
   (get' i m = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  m2 : tree' A
  j : positive
  H : xO i <> xI j
  ============================
   (get' i m1 = get' i m1)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  a : A
  j : positive
  H : xO i <> xI j
  ============================
   (get' i m = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  a : A
  m2 : tree' A
  j : positive
  H : xO i <> xI j
  ============================
   (get' i m1 = get' i m1)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  H : xO i <> xO j
  ============================
   (get' i (set0 j x) = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  j : positive
  H : xO i <> xO j
  ============================
   (get' i (set0 j x) = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  m : tree' A
  j : positive
  H : xO i <> xO j
  ============================
   (get' i (set0 j x) = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  H : xO i <> xO j
  ============================
   (get' i (set' j x m) = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  m2 : tree' A
  j : positive
  H : xO i <> xO j
  ============================
   (get' i (set' j x m1) = get' i m1)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  a : A
  j : positive
  H : xO i <> xO j
  ============================
   (get' i (set' j x m) = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  a : A
  m2 : tree' A
  j : positive
  H : xO i <> xO j
  ============================
   (get' i (set' j x m1) = get' i m1)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  H : xO i <> xH
  ============================
   (None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  H : xO i <> xH
  ============================
   (None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  m : tree' A
  H : xO i <> xH
  ============================
   (None = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  H : xO i <> xH
  ============================
   (get' i m = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  m2 : tree' A
  H : xO i <> xH
  ============================
   (get' i m1 = get' i m1)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  a : A
  H : xO i <> xH
  ============================
   (get' i m = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  a : A
  m2 : tree' A
  H : xO i <> xH
  ============================
   (get' i m1 = get' i m1)

    A : Type  x : A  m : tree' A  j : positive  H : xH <> xI j
  ============================
   (None = None)

    A : Type  x : A  a : A  j : positive  H : xH <> xI j
  ============================
   (Some a = Some a)

    A : Type  x : A  a : A  m : tree' A  j : positive  H : xH <> xI j
  ============================
   (Some a = Some a)

    A : Type  x : A  m : tree' A  j : positive  H : xH <> xI j
  ============================
   (None = None)

    A : Type  x : A  m1 : tree' A  m2 : tree' A  j : positive  H : xH <> xI j
  ============================
   (None = None)

    A : Type  x : A  m : tree' A  a : A  j : positive  H : xH <> xI j
  ============================
   (Some a = Some a)

  
  A : Type
  x : A
  m1 : tree' A
  a : A
  m2 : tree' A
  j : positive
  H : xH <> xI j
  ============================
   (Some a = Some a)

    A : Type  x : A  m : tree' A  j : positive  H : xH <> xO j
  ============================
   (None = None)

    A : Type  x : A  a : A  j : positive  H : xH <> xO j
  ============================
   (Some a = Some a)

    A : Type  x : A  a : A  m : tree' A  j : positive  H : xH <> xO j
  ============================
   (Some a = Some a)

    A : Type  x : A  m : tree' A  j : positive  H : xH <> xO j
  ============================
   (None = None)

    A : Type  x : A  m1 : tree' A  m2 : tree' A  j : positive  H : xH <> xO j
  ============================
   (None = None)

    A : Type  x : A  m : tree' A  a : A  j : positive  H : xH <> xO j
  ============================
   (Some a = Some a)

  
  A : Type
  x : A
  m1 : tree' A
  a : A
  m2 : tree' A
  j : positive
  H : xH <> xO j
  ============================
   (Some a = Some a)

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

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

    A : Type  x : A  a : A  m : tree' A  H : xH <> xH
  ============================
   (Some x = Some a)

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

    A : Type  x : A  m1 : tree' A  m2 : tree' A  H : xH <> xH
  ============================
   (Some x = None)

    A : Type  x : A  m : tree' A  a : A  H : xH <> xH
  ============================
   (Some x = Some a)

    A : Type  x : A  m1 : tree' A  a : A  m2 : tree' A  H : xH <> xH
  ============================
   (Some x = Some a)


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

Goals:
  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  H : xI i <> xI j
  ============================
   (get' i (set' j x m) = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  j : positive
  H : xI i <> xI j
  ============================
   (get' i (set0 j x) = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  m : tree' A
  j : positive
  H : xI i <> xI j
  ============================
   (get' i (set' j x m) = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  H : xI i <> xI j
  ============================
   (get' i (set0 j x) = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  m2 : tree' A
  j : positive
  H : xI i <> xI j
  ============================
   (get' i (set' j x m2) = get' i m2)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  a : A
  j : positive
  H : xI i <> xI j
  ============================
   (get' i (set0 j x) = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  a : A
  m2 : tree' A
  j : positive
  H : xI i <> xI j
  ============================
   (get' i (set' j x m2) = get' i m2)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  H : xO i <> xO j
  ============================
   (get' i (set0 j x) = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  j : positive
  H : xO i <> xO j
  ============================
   (get' i (set0 j x) = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  a : A
  m : tree' A
  j : positive
  H : xO i <> xO j
  ============================
   (get' i (set0 j x) = None)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  j : positive
  H : xO i <> xO j
  ============================
   (get' i (set' j x m) = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  m2 : tree' A
  j : positive
  H : xO i <> xO j
  ============================
   (get' i (set' j x m1) = get' i m1)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m : tree' A
  a : A
  j : positive
  H : xO i <> xO j
  ============================
   (get' i (set' j x m) = get' i m)

  
  A : Type
  i : positive
  x : A
  IHi : forall (m : tree' A) (j : positive),
        i <> j -> get' i (set' j x m) = get' i m
  m1 : tree' A
  a : A
  m2 : tree' A
  j : positive
  H : xO i <> xO j
  ============================
   (get' i (set' j x m1) = get' i m1)

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

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

    A : Type  x : A  a : A  m : tree' A  H : xH <> xH
  ============================
   (Some x = Some a)

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

    A : Type  x : A  m1 : tree' A  m2 : tree' A  H : xH <> xH
  ============================
   (Some x = None)

    A : Type  x : A  m : tree' A  a : A  H : xH <> xH
  ============================
   (Some x = Some a)

    A : Type  x : A  m1 : tree' A  a : A  m2 : tree' A  H : xH <> xH
  ============================
   (Some x = Some a)


DEBUG:Going to execute:
solve
[ apply IHi; congruence | apply gso0; congruence | congruence ]