- Consider the following definition of even natural numbers:
Inductive even : nat -> Prop := even0 : even 0 | even_S : forall p, even p -> even (S (S p)). Hint Constructors even.

Prove that the tower of height 6 is an even number, and let us call your theorem`six_tower`. -
Try the command
`Eval compute in six_tower` -
Make the constant
`six_tower`transparent (by replacing its`Qed`with`Defined`), and redo the preceding question. -
I presume that your proof of
`six_tower`uses some lemmas. Edit your proof and replace their`Qed`with`Defined`. What happens?

Going home