Goal:
    m : t  l : list t
  ============================
   (forall n : t, fold_left max l n = m -> n = m \/ In m l)


DEBUG:Going to execute:
induction l

Goals:
    m : t
  ============================
   (forall n : t, fold_left max [] n = m -> n = m \/ In m [])

  
  m : t
  a : t
  l : list t
  IHl : forall n : t, fold_left max l n = m -> n = m \/ In m l
  ============================
   (forall n : t, fold_left max (a :: l) n = m -> n = m \/ In m (a :: l))


DEBUG:Going to execute:
cbn
DEBUG LTAC Evaluated term: l

Goals:
    m : t
  ============================
   (forall n : t, n = m -> n = m \/ False)

  
  m : t
  a : t
  l : list t
  IHl : forall n : t, fold_left max l n = m -> n = m \/ In m l
  ============================
   (forall n : t, fold_left max l (max n a) = m -> n = m \/ a = m \/ In m l)


DEBUG:Going to execute:
intros n H