def Refl

bend-kit-collections@0.1.4.1 · PROOF.bend:208

import Base

208def Refl(~K: Data, ~cmp: K -> K -> Cmp) -> Type:
209  @x: K -> {cmp(x, x) == EQ{} : Cmp}