law pntake

lawful-fields@0.1.1.0 · proof_cut.bend:367

import lawful-fields@0.1.1.0/proof_cut.bend as ProofCut
import Base

367law pntake:
368  for +ns: List<&2, Nat>
369  for +n: Nat
370  for +xs: List<&2, U32>
371  for +s: Nat
372  {PN(List.take(&2, Nat, ns, n), xs, s) == List.take(&2, List<&2, U32>, PN(ns, xs, s), n) : List<&2, List<&2, U32>>}

Uses (8)

Used by (1)