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


DEBUG:Going to execute:
intros; symmetry
DEBUG LTAC Evaluated term: extensionality_empty