example: ∀ {t}, 0 ≤ t := by
  have : True := trivial
  sorry