Add proofs for quantifier identities

[michaelgwelch]

I think these are good practice before tackling the final proof of Session 6. Plus the second one can be used in the final proof.

Note: I haven't built locally yet to test that I don't have a typo. I'll do as soon as I can. I have some environment setup I need to do before I can build. Notably I don't have ghcjs installed.

[michaelgwelch]

I see the attempts to fix the build did not work. I'll wait til I see a successful build on travis, and rebase again on top of whatever fix is required.

[nomeata]

Ok, I think we fixed master.

[michaelgwelch]

Rebased