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


DEBUG:Going to execute:
induction i

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

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

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


DEBUG:Going to execute:
destruct j

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

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

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

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

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

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

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

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

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


DEBUG:Going to execute:
induction m using tree_ind

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

  
  A : Type
  i : positive
  IHi : forall (j : positive) (x : A) (m : tree A),
        i <> j -> get i (set j x m) = get i m
  j : positive
  x : A
  m1 : tree A
  o : option A
  m2 : tree A
  H : not_trivially_empty m1 o m2
  IHm1 : xI i <> xI j -> get (xI i) (set (xI j) x m1) = get (xI i) m1
  IHm2 : xI i <> xI j -> get (xI i) (set (xI j) x m2) = get (xI i) m2
  ============================
   (xI i <> xI j ->
    get (xI i) (set (xI j) x (Node m1 o m2)) = get (xI i) (Node m1 o m2))

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

  
  A : Type
  i : positive
  IHi : forall (j : positive) (x : A) (m : tree A),
        i <> j -> get i (set j x m) = get i m
  j : positive
  x : A
  m1 : tree A
  o : option A
  m2 : tree A
  H : not_trivially_empty m1 o m2
  IHm1 : xI i <> xO j -> get (xI i) (set (xO j) x m1) = get (xI i) m1
  IHm2 : xI i <> xO j -> get (xI i) (set (xO j) x m2) = get (xI i) m2
  ============================
   (xI i <> xO j ->
    get (xI i) (set (xO j) x (Node m1 o m2)) = get (xI i) (Node m1 o m2))

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

  
  A : Type
  i : positive
  IHi : forall (j : positive) (x : A) (m : tree A),
        i <> j -> get i (set j x m) = get i m
  x : A
  m1 : tree A
  o : option A
  m2 : tree A
  H : not_trivially_empty m1 o m2
  IHm1 : xI i <> xH -> get (xI i) (set xH x m1) = get (xI i) m1
  IHm2 : xI i <> xH -> get (xI i) (set xH x m2) = get (xI i) m2
  ============================
   (xI i <> xH ->
    get (xI i) (set xH x (Node m1 o m2)) = get (xI i) (Node m1 o m2))

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

  
  A : Type
  i : positive
  IHi : forall (j : positive) (x : A) (m : tree A),
        i <> j -> get i (set j x m) = get i m
  j : positive
  x : A
  m1 : tree A
  o : option A
  m2 : tree A
  H : not_trivially_empty m1 o m2
  IHm1 : xO i <> xI j -> get (xO i) (set (xI j) x m1) = get (xO i) m1
  IHm2 : xO i <> xI j -> get (xO i) (set (xI j) x m2) = get (xO i) m2
  ============================
   (xO i <> xI j ->
    get (xO i) (set (xI j) x (Node m1 o m2)) = get (xO i) (Node m1 o m2))

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

  
  A : Type
  i : positive
  IHi : forall (j : positive) (x : A) (m : tree A),
        i <> j -> get i (set j x m) = get i m
  j : positive
  x : A
  m1 : tree A
  o : option A
  m2 : tree A
  H : not_trivially_empty m1 o m2
  IHm1 : xO i <> xO j -> get (xO i) (set (xO j) x m1) = get (xO i) m1
  IHm2 : xO i <> xO j -> get (xO i) (set (xO j) x m2) = get (xO i) m2
  ============================
   (xO i <> xO j ->
    get (xO i) (set (xO j) x (Node m1 o m2)) = get (xO i) (Node m1 o m2))

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

  
  A : Type
  i : positive
  IHi : forall (j : positive) (x : A) (m : tree A),
        i <> j -> get i (set j x m) = get i m
  x : A
  m1 : tree A
  o : option A
  m2 : tree A
  H : not_trivially_empty m1 o m2
  IHm1 : xO i <> xH -> get (xO i) (set xH x m1) = get (xO i) m1
  IHm2 : xO i <> xH -> get (xO i) (set xH x m2) = get (xO i) m2
  ============================
   (xO i <> xH ->
    get (xO i) (set xH x (Node m1 o m2)) = get (xO i) (Node m1 o m2))

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

  
  A : Type
  j : positive
  x : A
  m1 : tree A
  o : option A
  m2 : tree A
  H : not_trivially_empty m1 o m2
  IHm1 : xH <> xI j -> get xH (set (xI j) x m1) = get xH m1
  IHm2 : xH <> xI j -> get xH (set (xI j) x m2) = get xH m2
  ============================
   (xH <> xI j ->
    get xH (set (xI j) x (Node m1 o m2)) = get xH (Node m1 o m2))

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

  
  A : Type
  j : positive
  x : A
  m1 : tree A
  o : option A
  m2 : tree A
  H : not_trivially_empty m1 o m2
  IHm1 : xH <> xO j -> get xH (set (xO j) x m1) = get xH m1
  IHm2 : xH <> xO j -> get xH (set (xO j) x m2) = get xH m2
  ============================
   (xH <> xO j ->
    get xH (set (xO j) x (Node m1 o m2)) = get xH (Node m1 o m2))

    A : Type  x : A
  ============================
   (xH <> xH -> get xH (set xH x Empty) = get xH Empty)

  
  A : Type
  x : A
  m1 : tree A
  o : option A
  m2 : tree A
  H : not_trivially_empty m1 o m2
  IHm1 : xH <> xH -> get xH (set xH x m1) = get xH m1
  IHm2 : xH <> xH -> get xH (set xH x m2) = get xH m2
  ============================
   (xH <> xH -> get xH (set xH x (Node m1 o m2)) = get xH (Node m1 o m2))


DEBUG:Going to execute:
intros
DEBUG LTAC Evaluated term: tree_ind
DEBUG LTAC Evaluated term: tree_ind
DEBUG LTAC Evaluated term: tree_ind
DEBUG LTAC Evaluated term: tree_ind
DEBUG LTAC Evaluated term: tree_ind
DEBUG LTAC Evaluated term: tree_ind
DEBUG LTAC Evaluated term: tree_ind
DEBUG LTAC Evaluated term: tree_ind
DEBUG LTAC Evaluated term: tree_ind

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

  
  A : Type
  i : positive
  IHi : forall (j : positive) (x : A) (m : tree A),
        i <> j -> get i (set j x m) = get i m
  j : positive
  x : A
  m1 : tree A
  o : option A
  m2 : tree A
  H : not_trivially_empty m1 o m2
  IHm1 : xI i <> xI j -> get (xI i) (set (xI j) x m1) = get (xI i) m1
  IHm2 : xI i <> xI j -> get (xI i) (set (xI j) x m2) = get (xI i) m2
  H0 : xI i <> xI j
  ============================
   (get (xI i) (set (xI j) x (Node m1 o m2)) = get (xI i) (Node m1 o m2))

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

  
  A : Type
  i : positive
  IHi : forall (j : positive) (x : A) (m : tree A),
        i <> j -> get i (set j x m) = get i m
  j : positive
  x : A
  m1 : tree A
  o : option A
  m2 : tree A
  H : not_trivially_empty m1 o m2
  IHm1 : xI i <> xO j -> get (xI i) (set (xO j) x m1) = get (xI i) m1
  IHm2 : xI i <> xO j -> get (xI i) (set (xO j) x m2) = get (xI i) m2
  H0 : xI i <> xO j
  ============================
   (get (xI i) (set (xO j) x (Node m1 o m2)) = get (xI i) (Node m1 o m2))

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

  
  A : Type
  i : positive
  IHi : forall (j : positive) (x : A) (m : tree A),
        i <> j -> get i (set j x m) = get i m
  x : A
  m1 : tree A
  o : option A
  m2 : tree A
  H : not_trivially_empty m1 o m2
  IHm1 : xI i <> xH -> get (xI i) (set xH x m1) = get (xI i) m1
  IHm2 : xI i <> xH -> get (xI i) (set xH x m2) = get (xI i) m2
  H0 : xI i <> xH
  ============================
   (get (xI i) (set xH x (Node m1 o m2)) = get (xI i) (Node m1 o m2))

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

  
  A : Type
  i : positive
  IHi : forall (j : positive) (x : A) (m : tree A),
        i <> j -> get i (set j x m) = get i m
  j : positive
  x : A
  m1 : tree A
  o : option A
  m2 : tree A
  H : not_trivially_empty m1 o m2
  IHm1 : xO i <> xI j -> get (xO i) (set (xI j) x m1) = get (xO i) m1
  IHm2 : xO i <> xI j -> get (xO i) (set (xI j) x m2) = get (xO i) m2
  H0 : xO i <> xI j
  ============================
   (get (xO i) (set (xI j) x (Node m1 o m2)) = get (xO i) (Node m1 o m2))

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

  
  A : Type
  i : positive
  IHi : forall (j : positive) (x : A) (m : tree A),
        i <> j -> get i (set j x m) = get i m
  j : positive
  x : A
  m1 : tree A
  o : option A
  m2 : tree A
  H : not_trivially_empty m1 o m2
  IHm1 : xO i <> xO j -> get (xO i) (set (xO j) x m1) = get (xO i) m1
  IHm2 : xO i <> xO j -> get (xO i) (set (xO j) x m2) = get (xO i) m2
  H0 : xO i <> xO j
  ============================
   (get (xO i) (set (xO j) x (Node m1 o m2)) = get (xO i) (Node m1 o m2))

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

  
  A : Type
  i : positive
  IHi : forall (j : positive) (x : A) (m : tree A),
        i <> j -> get i (set j x m) = get i m
  x : A
  m1 : tree A
  o : option A
  m2 : tree A
  H : not_trivially_empty m1 o m2
  IHm1 : xO i <> xH -> get (xO i) (set xH x m1) = get (xO i) m1
  IHm2 : xO i <> xH -> get (xO i) (set xH x m2) = get (xO i) m2
  H0 : xO i <> xH
  ============================
   (get (xO i) (set xH x (Node m1 o m2)) = get (xO i) (Node m1 o m2))

    A : Type  j : positive  x : A  H : xH <> xI j
  ============================
   (get xH (set (xI j) x Empty) = get xH Empty)

  
  A : Type
  j : positive
  x : A
  m1 : tree A
  o : option A
  m2 : tree A
  H : not_trivially_empty m1 o m2
  IHm1 : xH <> xI j -> get xH (set (xI j) x m1) = get xH m1
  IHm2 : xH <> xI j -> get xH (set (xI j) x m2) = get xH m2
  H0 : xH <> xI j
  ============================
   (get xH (set (xI j) x (Node m1 o m2)) = get xH (Node m1 o m2))

    A : Type  j : positive  x : A  H : xH <> xO j
  ============================
   (get xH (set (xO j) x Empty) = get xH Empty)

  
  A : Type
  j : positive
  x : A
  m1 : tree A
  o : option A
  m2 : tree A
  H : not_trivially_empty m1 o m2
  IHm1 : xH <> xO j -> get xH (set (xO j) x m1) = get xH m1
  IHm2 : xH <> xO j -> get xH (set (xO j) x m2) = get xH m2
  H0 : xH <> xO j
  ============================
   (get xH (set (xO j) x (Node m1 o m2)) = get xH (Node m1 o m2))

    A : Type  x : A  H : xH <> xH
  ============================
   (get xH (set xH x Empty) = get xH Empty)

  
  A : Type
  x : A
  m1 : tree A
  o : option A
  m2 : tree A
  H : not_trivially_empty m1 o m2
  IHm1 : xH <> xH -> get xH (set xH x m1) = get xH m1
  IHm2 : xH <> xH -> get xH (set xH x m2) = get xH m2
  H0 : xH <> xH
  ============================
   (get xH (set xH x (Node m1 o m2)) = get xH (Node m1 o m2))


DEBUG:Going to execute:
rewrite set_Empty || rewrite set_Node