any_goals
  solve
  | repeat'
      first
      | apply Even.add_two
      | apply Even.zero
case left

⊢ Even 4

case right.left

⊢ Even 7

case right.right.left

⊢ Even 3

case right.right.right

⊢ Even 0
case right.left

⊢ Even 7

case right.right.left

⊢ Even 3