Compare proof assistants (e.g., Coq, HOL, Lean) for proving inference rules in a given logical basis

[bhpayne]

This would be after addressing #199

https://en.wikipedia.org/wiki/Coq

https://hol-theorem-prover.org/

http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial.pdf https://github.com/jrh13/hol-light

HOL light Docker image posted to https://hub.docker.com/r/lcdoutlet/hol-light/

An OCaml-only image using Alpine: https://hub.docker.com/r/benislocated/ocaml/