The following excerpt comes from Sheaves and Logic by Fourman and Scott (Applications of Sheaves (1977), pag. 304):
I can't figure out where those two rules play a role in the proof that the powerset is a complete Heyting algebra but not its dual. Also, is there a nice example that the second law is not constructive?
The first one doesn't play a role, it's just an example to instanciate the fact that the powerset is a complete Heyting algebra.
The second one, however, shows that the dual is not a complete Heyting algebra, because if it were, then this law $\forall x [\phi\lor \psi(x)] \to \phi\lor\forall x\psi(x)$ would hold.
Indeed this asserts (in a sense) $\bigwedge_x (a\lor b(x)) \leq a\lor \bigwedge_x b(x)$, which in the dual poset means precisely $a\land \bigvee_x b(x)\leq \bigvee_x (a\land b(x))$ which is true in a cHa : indeed it is true if and only if $\bigvee_x b(x)\leq (a\implies \bigvee_x (a\land b(x)))$; and now you can take an $x$ and see that $b(x)$ is indeed smaller than the right hand side (with the same kind of trick)
As for an example where the second law doesn't hold, since you're reading about sheaves, here's an example from topology :
If the law were true, then for any topological space $X$, any open $U$, and any family $V_i, i\in I$ of opens, we would have $\mathrm{Int}(\displaystyle\bigcap_{i\in I} (U\cup V_i))\subset U\cup \mathrm{Int}(\displaystyle\bigcap_{i\in I}V_i)$. But this is not true, as the following example shows:
Take $X=\mathbb{R}$, $U= (0,1)$ and for $i\in \mathbb{N}$, $V_i= (1-\frac{1}{2^i}, 2)$, and $x=1$.
Then $x\notin U$, and $\displaystyle\bigcap_{i\in \mathbb{N}}V_i = [1, 2)$, so $x$ is not in its interior.
However, $U\cap V_i = (0,2)$ and so $x\in \mathrm{Int}(\displaystyle\bigcap_{i\in\mathbb{N}}U\cup V_i)$
EDIT : Ok so how does this prove anything ? Well it turns out that constructive logic is closely related to topology in the following sense : take a standard first order language; and for simplification I'll assume its only nonlogical symbol is a unary relation symbol $P$.
Also take a topological space $X$ and a domain $D$. For each $d\in D$, choose an open set $[|P(x) ; d|]$ in $X$. You may then assign an open set to each first order formula (with an assignment for each of its free variables) inductively in the "obvious" way, e.g. $[| \phi\land \psi; d_1,...,d_n|] := [|\phi; d_1,...,d_n|]\cap [|\psi; d_1,...,d_n|]$, similarly for $\lor$, for $\neg$ you take the interior of the complement (the complement is not open in general !), fo $\exists$ you take the union over $D$, for $\forall$ you take the interior of the intersection over $D$, and for $[|\phi \implies\psi|]$ you take the largest open set $U$ such that $U\cap [|\phi|]\subset [|\psi|]$ (which can be seen as the interior of $[|\phi|]^c \cup [|\psi|]$)
This gives you, for each first order formula, an open set of $X$, which can be seen as the "truth value" of that formula. If a formula is assigned $X$, then it's "true" : it holds everywhere, if it's assigned $\emptyset$, it's false : it holds nowhere.
Now you can prove the following soundness theorem : if $A\implies B$ is provable from intuitionistic logic, then for any such "model" (for any topological space, any assignment of the atomic formulas,..), $[|A|]\subset [|B|]$. It's really not that hard and follows basically from the definitions.
Here I found a model where the interpretation of the left hand side of the implication was not included in the interpretation of the right hand side, so by the soundness theorem the implication is not provable. Note that this proves that the law of excluded middle is not derivable from the rest of the axioms : indeed in most topological spaces, $[|p\lor \neg p|]\neg X$ for a general $p$ (i.e. the complement of an open is not generally open)