Goal:
  
  ============================
   (forall (A : Type) (m : tree' A), exists i : positive, get' i m <> None)


DEBUG:Going to execute:
induction m

Goals:
    A : Type  m : tree' A  IHm : exists i : positive, get' i m <> None
  ============================
   (exists i : positive, get' i (Node001 m) <> None)

    A : Type  a : A
  ============================
   (exists i : positive, get' i (Node010 a) <> None)

    A : Type  a : A  m : tree' A  IHm : exists i : positive, get' i m <> None
  ============================
   (exists i : positive, get' i (Node011 a m) <> None)

    A : Type  m : tree' A  IHm : exists i : positive, get' i m <> None
  ============================
   (exists i : positive, get' i (Node100 m) <> None)

  
  A : Type
  m1 : tree' A
  m2 : tree' A
  IHm1 : exists i : positive, get' i m1 <> None
  IHm2 : exists i : positive, get' i m2 <> None
  ============================
   (exists i : positive, get' i (Node101 m1 m2) <> None)

    A : Type  m : tree' A  a : A  IHm : exists i : positive, get' i m <> None
  ============================
   (exists i : positive, get' i (Node110 m a) <> None)

  
  A : Type
  m1 : tree' A
  a : A
  m2 : tree' A
  IHm1 : exists i : positive, get' i m1 <> None
  IHm2 : exists i : positive, get' i m2 <> None
  ============================
   (exists i : positive, get' i (Node111 m1 a m2) <> None)


DEBUG:Going to execute:
simpl

Goals:
    A : Type  m : tree' A  IHm : exists i : positive, get' i m <> None
  ============================
   (exists i : positive, get' i (Node001 m) <> None)

    A : Type  a : A
  ============================
   (exists i : positive, get' i (Node010 a) <> None)

    A : Type  a : A  m : tree' A  IHm : exists i : positive, get' i m <> None
  ============================
   (exists i : positive, get' i (Node011 a m) <> None)

    A : Type  m : tree' A  IHm : exists i : positive, get' i m <> None
  ============================
   (exists i : positive, get' i (Node100 m) <> None)

  
  A : Type
  m1 : tree' A
  m2 : tree' A
  IHm1 : exists i : positive, get' i m1 <> None
  IHm2 : exists i : positive, get' i m2 <> None
  ============================
   (exists i : positive, get' i (Node101 m1 m2) <> None)

    A : Type  m : tree' A  a : A  IHm : exists i : positive, get' i m <> None
  ============================
   (exists i : positive, get' i (Node110 m a) <> None)

  
  A : Type
  m1 : tree' A
  a : A
  m2 : tree' A
  IHm1 : exists i : positive, get' i m1 <> None
  IHm2 : exists i : positive, get' i m2 <> None
  ============================
   (exists i : positive, get' i (Node111 m1 a m2) <> None)


DEBUG:Going to execute:
try destruct IHm as [p H]