I am looking for examples of proofs or constructions that rely on a Heyting algebra. Furthermore, said examples must use the fact that Heyting algebras can be considered semantics for IPC, but be outside the study scope of IPC.
An example that does not fit the above criteria would be the construction of the Lindenbaum algebra from propositional formulae, because it is used to prove completeness.
An example that might fit the above criteria would be the fact that every Heyting algebra can be transformed into a collection of open sets of a topological space. I don't know if this construction can be actually used outside of IPC, in conjuction with the fact that it also acts as semantics for IPC.
The way I see it, any construction that is available for all Heyting algebras will not fit the criteria. Maybe something that is dependent on the inner structure of a particular one.
Edit: Adding some motivation/clarification.
Didactic reasons. When a student of logic is first introduced to the concepts of syntax/semantics, it is difficult to provide examples of actually using the formal language, usually because the language is so limited to keep the simplicity. Classical propositional calculus does not offer such a richness of models as IPC, so I thought that at least with IPC semantics we can do something other than just derivations.