\(a : *) -> \(x : a) -> x