Coq has less built-in automation, but with Ltac it's possible to achieve impressive levels of automation through explicitly-crafted decision procedures, as demonstrated in Chlipala's CPDT and many of his papers.
- Existing automatic theorem provers often produced non-constructive proofs.
- Existing automatic theorem provers are mostly for FOL, so the gap to the much more powerful logics of Curry-Howard based provers is bigger than with weaker systems.
Have both problems been solved comprehensively as of January 2020?