law take_get

lawful-bytes@0.1.1.0 · proof_core.bend:143

import Base

143law take_get:
144  for +xs: List<&2, U32>
145  for +n: Nat
146  for +i: Nat
147  for +h: {Nat.is_lt(i, n) == True{} : Bool}
148  {List.get(&2, U32, List.take(&2, U32, xs, n), i) == List.get(&2, U32, xs, i) : Maybe<&2, U32>}