Lemma 1.4.7 (Soundness of Heyting semantics). Assuming that:

• $H$ is a Heyting algebra

• $v:L\to H$ is a valuation