Re: Cantor Diagonal Proof

[Follow-up set to sci.logic.]
On 08/04/2025 15:14, Julio Di Egidio wrote:

[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?

It's *equality induction* (just prove it explicitly).
The presentation remains a bit clumsy, but I think
at least the steps now are the essential ones.
Julio