[carnitine]

That’s not true either. Coq’s logic is significantly different to HoL.

[riku_iki]

hol meaning higher order logic (https://en.wikipedia.org/wiki/Higher-order_logic) not the lang of hol prover.