Goal:
    A : Type
  ============================
   (forall m1 m2 : tree A,
    (forall i : positive, get i m1 = get i m2) -> m1 = m2)


DEBUG:Going to execute:
induction m1 using tree_ind

Goals:
    A : Type
  ============================
   (forall m2 : tree A,
    (forall i : positive, get i Empty = get i m2) -> Empty = m2)

  
  A : Type
  m1_1 : tree A
  o : option A
  m1_2 : tree A
  H : not_trivially_empty m1_1 o m1_2
  IHm1_1 : forall m2 : tree A,
           (forall i : positive, get i m1_1 = get i m2) -> m1_1 = m2
  IHm1_2 : forall m2 : tree A,
           (forall i : positive, get i m1_2 = get i m2) -> m1_2 = m2
  ============================
   (forall m2 : tree A,
    (forall i : positive, get i (Node m1_1 o m1_2) = get i m2) ->
    Node m1_1 o m1_2 = m2)


DEBUG:Going to execute:
induction m2 using tree_ind
DEBUG LTAC Evaluated term: tree_ind

Goals:
    A : Type
  ============================
   ((forall i : positive, get i Empty = get i Empty) -> Empty = Empty)

  
  A : Type
  m2_1 : tree A
  o : option A
  m2_2 : tree A
  H : not_trivially_empty m2_1 o m2_2
  IHm2_1 : (forall i : positive, get i Empty = get i m2_1) -> Empty = m2_1
  IHm2_2 : (forall i : positive, get i Empty = get i m2_2) -> Empty = m2_2
  ============================
   ((forall i : positive, get i Empty = get i (Node m2_1 o m2_2)) ->
    Empty = Node m2_1 o m2_2)

  
  A : Type
  m1_1 : tree A
  o : option A
  m1_2 : tree A
  H : not_trivially_empty m1_1 o m1_2
  IHm1_1 : forall m2 : tree A,
           (forall i : positive, get i m1_1 = get i m2) -> m1_1 = m2
  IHm1_2 : forall m2 : tree A,
           (forall i : positive, get i m1_2 = get i m2) -> m1_2 = m2
  ============================
   ((forall i : positive, get i (Node m1_1 o m1_2) = get i Empty) ->
    Node m1_1 o m1_2 = Empty)

  
  A : Type
  m1_1 : tree A
  o : option A
  m1_2 : tree A
  H : not_trivially_empty m1_1 o m1_2
  IHm1_1 : forall m2 : tree A,
           (forall i : positive, get i m1_1 = get i m2) -> m1_1 = m2
  IHm1_2 : forall m2 : tree A,
           (forall i : positive, get i m1_2 = get i m2) -> m1_2 = m2
  m2_1 : tree A
  o0 : option A
  m2_2 : tree A
  H0 : not_trivially_empty m2_1 o0 m2_2
  IHm2_1 : (forall i : positive, get i (Node m1_1 o m1_2) = get i m2_1) ->
           Node m1_1 o m1_2 = m2_1
  IHm2_2 : (forall i : positive, get i (Node m1_1 o m1_2) = get i m2_2) ->
           Node m1_1 o m1_2 = m2_2
  ============================
   ((forall i : positive,
     get i (Node m1_1 o m1_2) = get i (Node m2_1 o0 m2_2)) ->
    Node m1_1 o m1_2 = Node m2_1 o0 m2_2)


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