{-# OPTIONS --without-K --safe #-} open import Relation.Binary using (Setoid) module Cfe.Judgement.Properties {c ℓ} (over : Setoid c ℓ) where