module Star where data Star {A : Set}(R : A -> A -> Set) : A -> A -> Set where rf : {x : A} -> Star R x x _<>_ : forall {x y z} -> R x y -> Star R y z -> Star R x z
