def AP.fin_le_ff

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

import Base

179def AP.fin_le_ff(c: Cmp) -> {Cmp.is_le(Word.cmp.fin(False{}, False{}, c)) == Cmp.is_le(c) : Bool}:
180  match c:
181    case LT{}:
182      {==}
183    case EQ{}:
184      {==}
185    case GT{}:
186      {==}