~/jendhub

def word_fin_t

lawful-words@0.1.0.0 · proof_word.bend:264

import lawful-words@0.1.0.0/proof_word.bend as ProofWord
import Base

264def word_fin_t(+ab: Bool, +bb: Bool, +t: Cmp, e: {Word.cmp.fin(ab, bb, t) == EQ{} : Cmp}) -> {t == EQ{} : Cmp}:
265  match t:
266    case LT{}:
267      Empty.absurd({LT{} == EQ{} : Cmp}, lt_ne_eq(e))
268    case EQ{}:
269      {==}
270    case GT{}:
271      Empty.absurd({GT{} == EQ{} : Cmp}, gt_ne_eq(e))

Uses (6)

Used by (1)