def uq.fin_le_ft

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

import Base

277def uq.fin_le_ft(c: Cmp) -> {Cmp.is_le(Word.cmp.fin(False{}, True{}, c)) == Cmp.is_le(c) : Bool}:
278  match c:
279    case LT{}:
280      {==}
281    case EQ{}:
282      {==}
283    case GT{}:
284      {==}