System λ→ t ::= x t → t e ::= x e e λ x : t . e System λω k ::= * t ::= a ∀ a : k . t e ::= x e e λ x : t . e Λ a : k . e System λPω e ::= x * e e ∀ x : e . e λ x : e . e