law run_le

lawful-bytes@0.1.1.0 · proof_fast_find.bend:252

import Base
import lawful-bytes@0.1.1.0/defs.bend as D

252law run_le:
253  for +xs: List<&2, U32>
254  for +c: U32
255  for +b: Bool
256  for +hb: {hd_eq(xs, c) == b : Bool}
257  {Nat.is_le(D.run_len(xs, c), List.length(&2, U32, xs)) == True{} : Bool}