module Lib.One where

record One : Set where
  constructor ⟨⟩