-- A uAgda file contains exactly one term.
-- by running uAgda <file> you'll get the normal form for the term, and its type.
-- Try it on this file.

\(A : *) -> A -> A