Theorem: AltChoose_zero_eq_one (BrownCs22/Homework/Hw8.lean)

State before:
⊢ ∀ (n : ℕ), (n A 0) = 1
Tactic:
simp [AltChoose]
State after:
no goals