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

State before:
⊢ nondec []
Tactic:
define
State after:
⊢ True

State before:
⊢ True
Tactic:
trivial
State after:
no goals