The statement functions (e.g. AND/NOT/OR) are defined before the equivalence classes. Technically, the functions can only be uniquely defined on the equivalence classes, so they should be defined afterwards.
Prove that the verifiable statements form a complete Heyting algebra.