def AP.fin_lt_xf

bend-osdev-array@0.1.0.1 · PROOF.bend:206

import Base

206def AP.fin_lt_xf(b: Bool, c: Cmp) -> {Cmp.is_lt(Word.cmp.fin(b, False{}, c)) == Cmp.is_lt(c) : Bool}:
207  match b c:
208    case False{} LT{}:
209      {==}
210    case False{} EQ{}:
211      {==}
212    case False{} GT{}:
213      {==}
214    case True{} LT{}:
215      {==}
216    case True{} EQ{}:
217      {==}
218    case True{} GT{}:
219      {==}