tests/lean/456.lean

def A : Sort u := { s : Prop // _ }