Thanks, Guillaume, for the prompt reply. I now understand that in the powerful logic of Coq (the Calculus of Inductive Constructions?) my axiom is inconsistent. However, the axiom k_eq is taken from combinatory logic, which *is* consistent, in the sense that there are equations which cannot be proved; one cannot prove S=K from the equations

Kxy = x

and

Sxyz = (xz)(yz) .

The issue is that Coq introduces stronger logical principles.

Part II of my book is in the style you suggest: all theorems in the book are there proved without any axioms, only rewriting. However, this is heavy for most readers, so Part I is for readers who understand little more than equational reasoning. Indeed, most proofs use a single tactic, that does no more than apply the axioms. At this moment, it seems that all of these proofs written in Coq are “informal” as they use an “inconsistent” axiom even though I am not using the stronger logical principles that expose the inconsistency. Is there a fragment of Coq (or a different proof assistant) in which the existing proofs become formal? In which consistency is restored?

Yours,

Barry