Goal:
  
  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
  i : positive
  H1 : get (xI i) (Node m1_1 o m1_2) = get (xI i) (Node m2_1 o0 m2_2)
  ============================
   (get i m1_2 = get i m2_2)


DEBUG:Going to execute:
rewrite !gNode in H1
DEBUG LTAC Evaluated term: (H1 (xI i))