Machine.run_inv: law of bend-lawful-stdlib@0.1.0.0
Import: import bend-lawful-stdlib@0.1.0.0/src/machine.bend as Machine
Lines 16-25 of bend-lawful-stdlib@0.1.0.0/src/machine.bend: https://jend.leeeet.dev/read.txt?path=bend-lawful-stdlib@0.1.0.0/src/machine.bend&start_line=16&end_line=25

import Base

# a step that keeps Inv keeps it over any input list
law run_inv:
  for ~S: Data
  for ~I: Data
  for ~step: S -> I -> S
  for ~Inv: S -> Type
  for ~keep: @s: S -> @i: I -> Inv(s) -> Inv(step(s, i))
  for xs: List<&2, I>
  for +s: S
  Inv(s) -> Inv(run(~S, ~I, ~step, s, xs))

Uses (2):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/machine.bend&name=run