law wk

lawful-fields@0.1.1.0 · proof_cut.bend:406

import Base

406# A lower bound may be lowered.
407law wk:
408  for +ns: List<&2, Nat>
409  for +a: Nat
410  for +a2: Nat
411  for +b: Nat
412  for +h: {Nat.is_le(a, a2) == True{} : Bool}
413  for +hw: {WN(ns, a2, b) == True{} : Bool}
414  {WN(ns, a, b) == True{} : Bool}