Library TAPL.Tactics.Examples

From TAPL Require Import Tactics.

Inductive even : nat → Prop :=
| even_O : even 0
| even_SS : ∀ n, even n → even (S (S n)).