~/jendhub

def step_inv

bend-ml-llama@0.2.1.0 · main.bend:580

import bend-ml-llama@0.2.1.0/main.bend as BendMlLlama
import Base

580def step_inv(+t: Nat, -p: Nat, -cap: Nat, e: {Nat.add(t, 1n+p) == cap : Nat}) -> {Nat.add(1n+t, p) == cap : Nat}:
581  %e : {1n+Nat.add(t, p) == _ : Nat}
582  add_succ(t, p)

Uses (3)

Used by (1)