Add support for Coq, Lean, and Isabelle/HOL

Given that these are proof assistants that are also full-fledged dependently typed programming languages, I think all three of these languages (and similar ones that I am unaware of) definitely belong here