law take_below

bend-ml-llama@0.2.1.0 · main.bend:1317

import Base

1317# PROOF: taking the first k candidates keeps a part of them.
1318law take_below:
1319  for +cs: List<&2, Cand>
1320  for +k: Nat
1321  for +n: Nat
1322  for +e: {True{} == below(cs, n) : Bool}
1323  {True{} == below(List.take(&2, Cand, cs, k), n) : Bool}