Julios Solution is Different, what is it? (Was: Online Playground for System F)

Hi,
The stanford solution to self application
looks quite different than Julios. Here
is the stanford solution:
\x:forall X.X->X.x[forall X.X->X] x
https://crypto.stanford.edu/~blynn/lambda/systemf.html
And here is Julios solution:
Let `F : forall (X Y : Type), X -> Y`, then we can
(almost) write `F F`.  Simple seems simple, it just
doesn't end well:
```coq
(** There exists a function
     from any type to any type! *)
Axiom F : forall (X Y : Type), X -> Y.
(** Any two types: might be False False if
     that's all there is, an uninhabited type. *)
Parameters (T U : Type).
(** Now we can prove False. *)
Definition absurd : False :=
   F (T -> U) False (F T U).
```
Whats the difference between the two solutions?
Lets rewrite Julios solution in System F.
He has a combinator 'F' with this type:
'F' : forall X.forall Y.(X -> Y)
His last statement has an expression:
(F T U) which reduces to a type (T -> U).
His last statement has a further expression:
(F (T -> U) False) which reduces to ((T -> U) -> False
Combining these two expressions, has the type False:
(F (T -> U) False (F T U)) : False
Whats the name of this construction?
Bye
Julio Di Egidio schrieb:

On 09/01/2025 17:07, Mild Shock wrote:

Dear Julio
>
I told you a dozen times that the scope of

 You truly are just a spamming piece of shit.
 Indeed now go back to sleep until I post my next one sporadic thing, then back to spamming your insanely automatic stupid shit all over the place for a couple of weeks, i.e. just as it's need to make me go away in disgust.
 You fucking piece of retarded shit, I wish you, chat GTP, and the whole fucking corporate nazi-retarded interest that is paying the job an incorporated ass cancer.
 *Plonk*
 -Julio
 

my thread is simple types. Why don't you
open a separate thread for your fetish
>
System F and/or Coq. I really don't care
about System F. You can play online with
System F here:
>
https://crypto.stanford.edu/~blynn/lambda/systemf.html
>
Get some Brains!