module impredicative where

open import impredicative.prop public
open import impredicative.logic public