dedukti-1.0.1: t/exemple.dk

T : Type.

U : Type.

[] U --> T -> T.

app : f : (T -> T) -> T -> T.

[] app --> f : U => x : T => f x.