Goal:
  
  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
  H0 : forall i : positive, get i Empty = get i (Node m2_1 o m2_2)
  ============================
   (Empty = Node m2_1 o m2_2)


DEBUG:Going to execute:
fun => <coq-core.plugins.ltac::symmetry@0>