Public theorem type and axiom checks