Does double negation distribute over disjunction intuitionistically? Does the following equivalence
$$\lnot \lnot (A \lor B) \leftrightarrow (\lnot \lnot A \lor \lnot \lnot B)$$
hold in propositional intuitionistic logic? And in propositional minimal logic? (In propositional classical logic this is obvious since $A \leftrightarrow \lnot\lnot A$ is classically provable.)
Actually I have a proof that $(\lnot \lnot A \lor \lnot \lnot B) \to \lnot \lnot (A \lor B)$
holds in propositional minimal logic, so I'm interested in the converse implication: 
$$\lnot \lnot (A \lor B) \to (\lnot \lnot A \lor \lnot \lnot B)$$
If it is minimally or/and intuitionistically provable, I would like a (reference to a) direct proof in natural deduction-style.

Before getting down to technicalities, in cases like this it is worth first thinking informally. So, should we expect $\lnot \lnot (A \lor B) \to (\lnot \lnot A \lor \lnot \lnot B)$ to hold intuitionistically, given an informal BHK-style understanding of the connectives? If we are in a position to rule out being able to refute $A \lor B$, does that mean we must already be in a position to rule out being able to refute $A$ or alternatively in a position to to rule out being able to refute $B$?
Intuitively(!) not. So that gives us a motivation for expecting the given wff to fail as an intuitionistic theorem, and hence to look for a Kripke counter model. And as Andreas Blass shows, once you start looking for a suitable model, given the constraints, you'll quickly land on one!
