module Elem where

open import Prelude
open import Star

Elem : {X : Set}(R : Rel X) -> Rel X
Elem R x y = Star (LeqBool [×] R) (false , x) (true , y)