Why does this following code doesn't type check?

Stream: new members

[Rui Liu]

A beginner question:

#check fun (A: Prop), fun (C: ∀ B: Prop, B), fun (x: (C A)), x

Why does this code doesn't type check? It's complaining at the (C A) part but I don't understand the error message.

[Kevin Buzzard]

C is a proof that all propositions are true, and C A is a proof that A is true, so it's not a type, so you can't talk about a term x of that type.

[Rui Liu]

Kevin Buzzard said:

C is a proof that all propositions are true, and C A is a proof that A is true, so it's not a type, so you can't talk about a term x of that type.

Thank you, I see now! An btw the natural number games are fantastic!