def Trans

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

import Base

202def Trans(~K: Data, ~cmp: K -> K -> Cmp) -> Type:
203  @x: K -> @y: K -> @z: K -> {cmp(x, y) == LT{} : Cmp} -> {cmp(y, z) == LT{} : Cmp} -> {cmp(x, z) == LT{} : Cmp}