def gt_ne_eq

lawful-words@0.1.0.0 · proof_word.bend:249

import Base

249def gt_ne_eq(e: {GT{} == EQ{} : Cmp}) -> Empty:
250  %e : Cmp.disc_eq(_)
251  Unit{}