A : Type.
[] A --> A -> A.
t : A.
[] t --> x : A => x.