Goal:
  
  a : Nbar.t
  l : list Nbar.t
  IHl : forall acc : Nbar.t,
        (Some 0 <= acc)%nbar -> (Some 0 <= fold_left max l acc)%nbar
  acc : Nbar.t
  H : (Some 0 <= acc)%nbar
  ============================
   (Some 0 <= max acc a)%nbar


DEBUG:Going to execute:
apply max_le'
DEBUG LTAC Evaluated term: IHl