Proof.done_eq: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/natural/proof.bend as Proof
Lines 33-35 of bend-collections-laws-math@1.0.0.0/proofs/math/natural/proof.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/proof.bend&start_line=33&end_line=35

import Base
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M

# a result that is Done twice holds one value
def done_eq(+t: Result<&2, &2, M.MathError, Nat>, +a: Nat, +b: Nat, +ha: {t == Done{a} : Result<&2, &2, M.MathError, Nat>}, +hb: {t == Done{b} : Result<&2, &2, M.MathError, Nat>}) -> {a == b : Nat}:
  Equal.cong(Result<&2, &2, M.MathError, Nat>, Nat, res_val, Done{a}, Done{b}, Equal.trans(Result<&2, &2, M.MathError, Nat>, Done{a}, t, Done{b}, Equal.sym(Result<&2, &2, M.MathError, Nat>, t, Done{a}, ha), hb))

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/proof.bend&name=res_val
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/natural.bend&name=MathError