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; induction m2 using tree_ind
DEBUG LTAC Evaluated term: (tree'_not_empty m)
DEBUG LTAC Evaluated term: GET
DEBUG LTAC Evaluated term: H