∀(record : { x : Type, y : Type → Type }) → Type