I thought that maybe if I started with an assumption []~p, I could somehow prove a contradiction and conclude ~[]~p, from where I could use disjunction introduction to get to the answer... but it did not take me anywhere.. this is a particularly tough one.. I'm obviously missing something small...
For the time being all I can say is it rings a bell... Yes, it has a similar form to the one from the exam (apart from the connective). I'll have to go bash away at it, and see whether I can find a way...
I think we go into the arbitrary world, and then reason in an ordinary way? So pick a target inside there that comes out as ... hmm. OK if the only thing that came out was diamond p, surely one could then conclude "diamond-p OR absolutely-anything" ?