Theorem: HTPI.prod_nil (HTPILib/Chap7.lean)

State before:
⊢ prod [] = 1
Tactic:
rfl
State after:
no goals