On the danger of evaluation

First define on nat the exponential towers of base 2 and heigth n. For instance the tower of height 4 is 2^{2^2²} =16384.

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?

Solution