\(a : Type) -> forall (b : a) -> a