data LAll : (a -> Type) -> List a -> Type
Nil : LAll p []
(::) : p x -@ (LAll p xs -@ LAll p (x :: xs))