···529529530530### Proving For All
531531532532-A few sections earlier, you've proven `birthYear + age = 2005` for this code:
532532+A few sections earlier, you've proven `birthYear + age = 2025` for this code:
533533534534```lean
535535def name := "Alice"