But in other theorem provers like, HOL Light, the distinction between a theorem and a term is rigorous. As I understand it, a term can only be of type theorem if it has actually been the output of a set of inference rules or tactics, but what I thought was weird is that Coq does not actually make this distinction explicit for some reason. Do you know why?
Wrote a related question: Why doesn't Coq have a theorem Type like HOL Light?