Question about page 122: Chapter 3.1, Exercise 22

[MetallicCrimson]

Since we're supposed to use the form
∀ __ x, if __, then __
I believe
Proof. ∀x, if x is a Java program, then x has at least 5 lines.
would be better as
Proof. ∀ program x, if x is a Java program, then x has at least 5 lines.
or
Proof. ∀ program x, if x is written in Java, then x has at least 5 lines.
since the original is correct, but it's not what the exercise is asking.

(But I wanted to mark this a question instead of a fix, because I might be wrong here.)

[spamegg1]

Closed by #44 thanks a lot!