def done_eq

bend-collections-laws-math@1.0.0.0 · proofs/math/natural/proof.bend:33

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

33# a result that is Done twice holds one value
34def 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}:
35  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))