In his example, `ZERO` is a value of type `zero even`. `ZERO` is the "proof" that zero is even. Of course its not much of a proof, rather its true by definition. Similarly `STEP ZERO` is of type `suc(suc(zero)) even` and thus a "proof" that two is even.
Comments
In his example, `ZERO` is a value of type `zero even`. `ZERO` is the "proof" that zero is even. Of course its not much of a proof, rather its true by definition. Similarly `STEP ZERO` is of type `suc(suc(zero)) even` and thus a "proof" that two is even.