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


DEBUG:Going to execute:
induction i

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

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

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


DEBUG:Going to execute:
simpl

Goals:
  
  A : Type
  i : positive
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j m) = get' i m
  j : positive
  m : tree' A
  ============================
   (xI i <> xI j -> get (xI i) (Node Empty None (rem' j m)) = get' i m)

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

  
  A : Type
  i : positive
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j m) = get' i m
  j : positive
  a : A
  m : tree' A
  ============================
   (xI i <> xI j -> get (xI i) (Node Empty (Some a) (rem' j m)) = get' i m)

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

  
  A : Type
  i : positive
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j m) = get' i m
  j : positive
  m1 : tree' A
  m2 : tree' A
  ============================
   (xI i <> xI j -> get (xI i) (Node (Nodes m1) None (rem' j m2)) = get' i m2)

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

  
  A : Type
  i : positive
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j m) = get' i m
  j : positive
  m1 : tree' A
  a : A
  m2 : tree' A
  ============================
   (xI i <> xI j ->
    get (xI i) (Node (Nodes m1) (Some a) (rem' j m2)) = get' i m2)

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

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

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

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

  
  A : Type
  i : positive
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j m) = get' i m
  j : positive
  m1 : tree' A
  m2 : tree' A
  ============================
   (xI i <> xO j -> get (xI i) (Node (rem' j m1) None (Nodes m2)) = get' i m2)

  
  A : Type
  i : positive
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j m) = get' i m
  j : positive
  m : tree' A
  a : A
  ============================
   (xI i <> xO j -> get (xI i) (Node (rem' j m) (Some a) Empty) = None)

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

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

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

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

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

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

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

  
  A : Type
  i : positive
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j 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
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j m) = get' i m
  j : positive
  m : tree' A
  ============================
   (xO i <> xI j -> get (xO i) (Node Empty None (rem' j m)) = None)

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

  
  A : Type
  i : positive
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j m) = get' i m
  j : positive
  a : A
  m : tree' A
  ============================
   (xO i <> xI j -> get (xO i) (Node Empty (Some a) (rem' j m)) = None)

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

  
  A : Type
  i : positive
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j m) = get' i m
  j : positive
  m1 : tree' A
  m2 : tree' A
  ============================
   (xO i <> xI j -> get (xO i) (Node (Nodes m1) None (rem' j m2)) = get' i m1)

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

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

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

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

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

  
  A : Type
  i : positive
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j m) = get' i m
  j : positive
  m : tree' A
  ============================
   (xO i <> xO j -> get (xO i) (Node (rem' j m) None Empty) = get' i m)

  
  A : Type
  i : positive
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j m) = get' i m
  j : positive
  m1 : tree' A
  m2 : tree' A
  ============================
   (xO i <> xO j -> get (xO i) (Node (rem' j m1) None (Nodes m2)) = get' i m1)

  
  A : Type
  i : positive
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j m) = get' i m
  j : positive
  m : tree' A
  a : A
  ============================
   (xO i <> xO j -> get (xO i) (Node (rem' j m) (Some a) Empty) = get' i m)

  
  A : Type
  i : positive
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j m) = get' i m
  j : positive
  m1 : tree' A
  a : A
  m2 : tree' A
  ============================
   (xO i <> xO j ->
    get (xO i) (Node (rem' j m1) (Some a) (Nodes m2)) = get' i m1)

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

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

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

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

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

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

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

    A : Type  j : positive  m : tree' A
  ============================
   (xH <> xI j -> get xH (Node Empty None (rem' j m)) = None)

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

    A : Type  j : positive  a : A  m : tree' A
  ============================
   (xH <> xI j -> get xH (Node Empty (Some a) (rem' j m)) = Some a)

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

    A : Type  j : positive  m1 : tree' A  m2 : tree' A
  ============================
   (xH <> xI j -> get xH (Node (Nodes m1) None (rem' j m2)) = None)

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

    A : Type  j : positive  m1 : tree' A  a : A  m2 : tree' A
  ============================
   (xH <> xI j -> get xH (Node (Nodes m1) (Some a) (rem' j m2)) = Some a)

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

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

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

    A : Type  j : positive  m : tree' A
  ============================
   (xH <> xO j -> get xH (Node (rem' j m) None Empty) = None)

    A : Type  j : positive  m1 : tree' A  m2 : tree' A
  ============================
   (xH <> xO j -> get xH (Node (rem' j m1) None (Nodes m2)) = None)

    A : Type  j : positive  m : tree' A  a : A
  ============================
   (xH <> xO j -> get xH (Node (rem' j m) (Some a) Empty) = Some a)

    A : Type  j : positive  m1 : tree' A  a : A  m2 : tree' A
  ============================
   (xH <> xO j -> get xH (Node (rem' j m1) (Some a) (Nodes m2)) = Some a)

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

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

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

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

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

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

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


DEBUG:Going to execute:
intros

Goals:
  
  A : Type
  i : positive
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j m) = get' i m
  j : positive
  m : tree' A
  H : xI i <> xI j
  ============================
   (get (xI i) (Node Empty None (rem' j m)) = get' i m)

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

  
  A : Type
  i : positive
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j m) = get' i m
  j : positive
  a : A
  m : tree' A
  H : xI i <> xI j
  ============================
   (get (xI i) (Node Empty (Some a) (rem' j m)) = get' i m)

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

  
  A : Type
  i : positive
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j m) = get' i m
  j : positive
  m1 : tree' A
  m2 : tree' A
  H : xI i <> xI j
  ============================
   (get (xI i) (Node (Nodes m1) None (rem' j m2)) = get' i m2)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  
  A : Type
  i : positive
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j 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
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j m) = get' i m
  j : positive
  m : tree' A
  H : xO i <> xI j
  ============================
   (get (xO i) (Node Empty None (rem' j m)) = None)

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

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

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

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

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

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

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

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

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

  
  A : Type
  i : positive
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j m) = get' i m
  j : positive
  m : tree' A
  H : xO i <> xO j
  ============================
   (get (xO i) (Node (rem' j m) None Empty) = get' i m)

  
  A : Type
  i : positive
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j m) = get' i m
  j : positive
  m1 : tree' A
  m2 : tree' A
  H : xO i <> xO j
  ============================
   (get (xO i) (Node (rem' j m1) None (Nodes m2)) = get' i m1)

  
  A : Type
  i : positive
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j m) = get' i m
  j : positive
  m : tree' A
  a : A
  H : xO i <> xO j
  ============================
   (get (xO i) (Node (rem' j m) (Some a) Empty) = get' i m)

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

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

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

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

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

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

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

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

    A : Type  j : positive  m : tree' A  H : xH <> xI j
  ============================
   (get xH (Node Empty None (rem' j m)) = None)

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

    A : Type  j : positive  a : A  m : tree' A  H : xH <> xI j
  ============================
   (get xH (Node Empty (Some a) (rem' j m)) = Some a)

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

    A : Type  j : positive  m1 : tree' A  m2 : tree' A  H : xH <> xI j
  ============================
   (get xH (Node (Nodes m1) None (rem' j m2)) = None)

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

    A : Type  j : positive  m1 : tree' A  a : A  m2 : tree' A  H : xH <> xI j
  ============================
   (get xH (Node (Nodes m1) (Some a) (rem' j m2)) = Some a)

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

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

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

    A : Type  j : positive  m : tree' A  H : xH <> xO j
  ============================
   (get xH (Node (rem' j m) None Empty) = None)

    A : Type  j : positive  m1 : tree' A  m2 : tree' A  H : xH <> xO j
  ============================
   (get xH (Node (rem' j m1) None (Nodes m2)) = None)

    A : Type  j : positive  m : tree' A  a : A  H : xH <> xO j
  ============================
   (get xH (Node (rem' j m) (Some a) Empty) = Some a)

    A : Type  j : positive  m1 : tree' A  a : A  m2 : tree' A  H : xH <> xO j
  ============================
   (get xH (Node (rem' j m1) (Some a) (Nodes m2)) = Some a)

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

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

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

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

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

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

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


DEBUG:Going to execute:
auto

Goals:
  
  A : Type
  i : positive
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j m) = get' i m
  j : positive
  m : tree' A
  H : xI i <> xI j
  ============================
   (get (xI i) (Node Empty None (rem' j m)) = get' i m)

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

  
  A : Type
  i : positive
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j m) = get' i m
  j : positive
  a : A
  m : tree' A
  H : xI i <> xI j
  ============================
   (get (xI i) (Node Empty (Some a) (rem' j m)) = get' i m)

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

  
  A : Type
  i : positive
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j m) = get' i m
  j : positive
  m1 : tree' A
  m2 : tree' A
  H : xI i <> xI j
  ============================
   (get (xI i) (Node (Nodes m1) None (rem' j m2)) = get' i m2)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  
  A : Type
  i : positive
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j 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
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j m) = get' i m
  j : positive
  m : tree' A
  H : xO i <> xI j
  ============================
   (get (xO i) (Node Empty None (rem' j m)) = None)

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

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

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

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

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

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

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

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

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

  
  A : Type
  i : positive
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j m) = get' i m
  j : positive
  m : tree' A
  H : xO i <> xO j
  ============================
   (get (xO i) (Node (rem' j m) None Empty) = get' i m)

  
  A : Type
  i : positive
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j m) = get' i m
  j : positive
  m1 : tree' A
  m2 : tree' A
  H : xO i <> xO j
  ============================
   (get (xO i) (Node (rem' j m1) None (Nodes m2)) = get' i m1)

  
  A : Type
  i : positive
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j m) = get' i m
  j : positive
  m : tree' A
  a : A
  H : xO i <> xO j
  ============================
   (get (xO i) (Node (rem' j m) (Some a) Empty) = get' i m)

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

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

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

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

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

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

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

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

    A : Type  j : positive  m : tree' A  H : xH <> xI j
  ============================
   (get xH (Node Empty None (rem' j m)) = None)

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

    A : Type  j : positive  a : A  m : tree' A  H : xH <> xI j
  ============================
   (get xH (Node Empty (Some a) (rem' j m)) = Some a)

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

    A : Type  j : positive  m1 : tree' A  m2 : tree' A  H : xH <> xI j
  ============================
   (get xH (Node (Nodes m1) None (rem' j m2)) = None)

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

    A : Type  j : positive  m1 : tree' A  a : A  m2 : tree' A  H : xH <> xI j
  ============================
   (get xH (Node (Nodes m1) (Some a) (rem' j m2)) = Some a)

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

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

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

    A : Type  j : positive  m : tree' A  H : xH <> xO j
  ============================
   (get xH (Node (rem' j m) None Empty) = None)

    A : Type  j : positive  m1 : tree' A  m2 : tree' A  H : xH <> xO j
  ============================
   (get xH (Node (rem' j m1) None (Nodes m2)) = None)

    A : Type  j : positive  m : tree' A  a : A  H : xH <> xO j
  ============================
   (get xH (Node (rem' j m) (Some a) Empty) = Some a)

    A : Type  j : positive  m1 : tree' A  a : A  m2 : tree' A  H : xH <> xO j
  ============================
   (get xH (Node (rem' j m1) (Some a) (Nodes m2)) = Some a)

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

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

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

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

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

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

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


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

Goals:
  
  A : Type
  i : positive
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j m) = get' i m
  j : positive
  m : tree' A
  H : xI i <> xI j
  ============================
   (get (xI i) (Node Empty None (rem' j m)) = get' i m)

  
  A : Type
  i : positive
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j m) = get' i m
  j : positive
  a : A
  m : tree' A
  H : xI i <> xI j
  ============================
   (get (xI i) (Node Empty (Some a) (rem' j m)) = get' i m)

  
  A : Type
  i : positive
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j m) = get' i m
  j : positive
  m1 : tree' A
  m2 : tree' A
  H : xI i <> xI j
  ============================
   (get (xI i) (Node (Nodes m1) None (rem' j m2)) = get' i m2)

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

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

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

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

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

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

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

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

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

  
  A : Type
  i : positive
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j m) = get' i m
  j : positive
  m : tree' A
  H : xO i <> xO j
  ============================
   (get (xO i) (Node (rem' j m) None Empty) = get' i m)

  
  A : Type
  i : positive
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j m) = get' i m
  j : positive
  m1 : tree' A
  m2 : tree' A
  H : xO i <> xO j
  ============================
   (get (xO i) (Node (rem' j m1) None (Nodes m2)) = get' i m1)

  
  A : Type
  i : positive
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j m) = get' i m
  j : positive
  m : tree' A
  a : A
  H : xO i <> xO j
  ============================
   (get (xO i) (Node (rem' j m) (Some a) Empty) = get' i m)

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

    A : Type  j : positive  m : tree' A  H : xH <> xI j
  ============================
   (get xH (Node Empty None (rem' j m)) = None)

    A : Type  j : positive  a : A  m : tree' A  H : xH <> xI j
  ============================
   (get xH (Node Empty (Some a) (rem' j m)) = Some a)

    A : Type  j : positive  m1 : tree' A  m2 : tree' A  H : xH <> xI j
  ============================
   (get xH (Node (Nodes m1) None (rem' j m2)) = None)

    A : Type  j : positive  m1 : tree' A  a : A  m2 : tree' A  H : xH <> xI j
  ============================
   (get xH (Node (Nodes m1) (Some a) (rem' j m2)) = Some a)

    A : Type  j : positive  m : tree' A  H : xH <> xO j
  ============================
   (get xH (Node (rem' j m) None Empty) = None)

    A : Type  j : positive  m1 : tree' A  m2 : tree' A  H : xH <> xO j
  ============================
   (get xH (Node (rem' j m1) None (Nodes m2)) = None)

    A : Type  j : positive  m : tree' A  a : A  H : xH <> xO j
  ============================
   (get xH (Node (rem' j m) (Some a) Empty) = Some a)

    A : Type  j : positive  m1 : tree' A  a : A  m2 : tree' A  H : xH <> xO j
  ============================
   (get xH (Node (rem' j m1) (Some a) (Nodes m2)) = Some a)

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

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

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

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


DEBUG:Going to execute:
solve [ congruence | rewrite gNode; auto; apply IHi; congruence ]