law wtake

lawful-fields@0.1.1.0 · proof_cut.bend:386

import Base

386law wtake:
387  for +ns: List<&2, Nat>
388  for +n: Nat
389  for +a: Nat
390  for +b: Nat
391  for +hw: {WN(ns, a, b) == True{} : Bool}
392  {WN(List.take(&2, Nat, ns, n), a, b) == True{} : Bool}