ev0: even 0

Question

我通过以下格式定义了偶数。

Inductive even : nat -> Prop :=
| ev0: even 0
| evSS: forall n, even n -> even S (S n) .

我想在列表中加入无穷大，所以就像这样 (even inf) 作为一个命题。我如何才能做到这一点？