Inductive even : nat -> Prop :=
| ev_0 : even 0
| ev_2 : even 2
| ev_sum : forall n m, even n -> even m -> even (n + m).