OK, eventually I see what you mean, and it’s a fine technical point: just, I wouldn’t read H
that way. Allow me to try and rephrase the whole thing:
<< Coq has conversion rules that can be used to determine if two terms are equal by definition in CIC, or convertible. >>
I read that as: “equality” in CIC, whence the built-in eq
in Coq, is synonym / realized-as / corresponds to “convertibility” (with the specific meaning/semantics as documented).
And I read H
, by definition of eq
as an inductive with the one constructor eq_refl
as carrier of (specific) evidence, as stating that, whatever x
and y
are in the context, H
is the assumption that we have a proof (evidence) that x
and y
(themselves) “unify”, i.e. are “convertible”… as well as e.g. rewrite
is defined in those terms, etc.
And, you rightly object that “no, not x
and y
themselves, just the terms x
and y
stand for…” (pardon the simple paraphrase, conducive to my argument…), which I find literally correct but simply beside the point re the meaning / (operational) semantics of eq and how it can ever ever be called a Leibniz equality…!?
(Not to mention, the docs seem to say otherwise in almost as many places, maybe again, depending on the level of discourse… And, the equivalence proved initially by @SkySkimmer, which, maybe wrongly, but I have proposed is evidence that there is no Leibniz, namely Extensionality, at all in the core language: aka it’s a purely intensional language… but here I start speculating.)