def cmp_eq_gt

bend-collections-laws-math@1.0.0.0 · proofs/lib/logic.bend:76

import Base

76def cmp_eq_gt(e: {EQ{} == GT{} : Cmp}) -> Empty:
77  %e : truth(Cmp.is_eq(_))
78  Unit{}