Comment Comment by carnitine That’s not true either. Coq’s logic is significantly different to HoL. parent carnitine 3 years ago