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
y are in the context,
H is the assumption that we have a proof (evidence) that
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
y themselves, just the terms
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.)