~/jendhub

def un.fin_eq_tail

bend-osdev-u32@0.1.0.0 · PROOF.bend:426

import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOF
import Base

426def un.fin_eq_tail(c: Cmp, -x: Bool, -y: Bool, e: {Word.cmp.fin(x, y, c) == EQ{} : Cmp}) -> {c == EQ{} : Cmp}:
427  match c:
428    case LT{}:
429      Empty.absurd({LT{} == EQ{} : Cmp}, un.lt_eq(e))
430    case EQ{}:
431      {==}
432    case GT{}:
433      Empty.absurd({GT{} == EQ{} : Cmp}, un.gt_eq(e))

Uses (6)

Used by (1)