law wn
import lawful-fields@0.1.1.0/proof_cut.bend as ProofCutimport Base
import lawful-fields@0.1.1.0/defs.bend as F
352law wn:
353 for +es: List<&2, U32>
354 for +a: Nat
355 for +b: Nat
356 {F.within(es, a, b) == WN(F.nats(es), a, b) : Bool}
import lawful-fields@0.1.1.0/proof_cut.bend as ProofCutimport Base
import lawful-fields@0.1.1.0/defs.bend as F
352law wn:
353 for +es: List<&2, U32>
354 for +a: Nat
355 for +b: Nat
356 {F.within(es, a, b) == WN(F.nats(es), a, b) : Bool}