Re: Cantor Diagonal Proof

[Cross-posted to sci-logic.  Please set follow-ups as needed.]
On 07/04/2025 17:16, Julio Di Egidio wrote:

My Gist, Cantor's diagonal argument (in Rocq):
<https://gist.github.com/jp-diegidio/eb05f6265c38b35c85853514ed46ab47>
<< We go for the simplest construction, which
    is not in terms of sets, just (type-theoretic)
    functions plus the most basic functional
    extensionality, i.e. eta-conversion. >>
 In fact, learning some formal mathematics with some tool
that supports it I think makes one's informal mathematics
way sharper, especially for those who are [self-taught]
(whatever that means).
 That said, I find my formalisation neither particularly
pretty nor particularly clear: corrections and suggestions
are welcome, especially in the direction of minimising
assumptions.

In particular, I think I am botching this:
```
(* given hypothesis [f = g] *)
assert (En : forall n, f n = g n)
   by congruence.    (** indisc. of ident. *)
```
That is not indiscernibility of identicals,
which rather looks like `forall P, P f = P g`,
but it's not eta-expansion either.  What is it?
Julio