Something went wrong. Try again.
Coding agent with a memory of all things
Something went wrong. Try again.
401 B · 9 lines
12345678910# eukhe: lemmas the proofs of two or more areas share: progress
import Baseimport ../../bend/progress.bend as Pr
# adding an act the ledger does not hold puts it in frontdef pp.add_new(+s: List<&2, Nat>, +x: Nat, m: {Pr.mem(x, s) == False{} : Bool}) -> {Pr.add(s, x) == x <> s : List<&2, Nat>}: %Equal.sym(Bool, Pr.mem(x, s), False{}, m) : {Pr.add.put(_, x, s) == x <> s : List<&2, Nat>} {==}