Question about type parameters to `Exists`

Stream: new members

[Rajiv]

I am trying to understand how Exists works in Lean.

In logic.lean Exists is defined as follows.

inductive Exists {α : Sort u} (p : α → Prop) : Prop
| intro (w : α) (h : p w) : Exists

Now in this example,

variable U : Type

variable A : U → U → Prop

variable a : ∃ (x : U) (y : U), A x y

#check a

What values would α and p take in the type constructor for Exists?

[Kenny Lau]

This is syntactic sugar for nested exists

[Kenny Lau]

you can put set_option pp.all true on the line before #check a

[Rajiv]

Thanks Kenny. I am really looking forward to going back to Haskell, after I understand lean type system! :-)