def uq.fin_le_ff

bend-osdev-algo@0.1.0.0 · proof_u32.bend:259

import Base

259def uq.fin_le_ff(c: Cmp) -> {Cmp.is_le(Word.cmp.fin(False{}, False{}, c)) == Cmp.is_le(c) : Bool}:
260  match c:
261    case LT{}:
262      {==}
263    case EQ{}:
264      {==}
265    case GT{}:
266      {==}