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


DEBUG:Going to execute:
induction l

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

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


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

Goals:
    n : t
  ============================
   (forall m : t, n <= m \/ Exists (le n) [] -> n <= m)

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


DEBUG:Going to execute:
intros m [H| H]