ParentFull threadcarnitine·That’s not true either. Coq’s logic is significantly different to HoL.View on HN