> sometimes what you want to prove is more convenient to express in the CoC. You can also express it in HOL, but not quite as easily. > All that said, automati

> sometimes what you want to prove is more convenient to express in the CoC. You can also express it in HOL, but not quite as easily. > All that said, automation of provers based on the LCF approach with a non-constructive logic is much superior as of December 2017. This is kind of the point I am making. Is the fact that some things are more convenient to express worth the substantial loss of automation? > With this in mind I was surprised to see that L. de Moura based the new Lean prover [2] on a variant of the CoC. He thinks that all automation that we currently have for HOL (i.e. Isabelle/HOL) can be brought to Lean. > J. Blanchette [3] seems to think the same. Interesting, thanks! I hope they are right and in the future this kind of automation does come to Coq and Lean.