def some_of

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fixgen.bend:24

import Base
import bend-collections-laws-math@1.0.0.0/src/math/fixed.bend as F
import bend-collections-laws-math@1.0.0.0/spec/math/fixed.bend as SF

24def some_of(~T: Data, ~val: T -> Nat, +bad: Bool, +hb: {bad == False{} : Bool}, +r: T, +n: Nat, +hv: {val(r) == n : Nat}) -> {SF.mval(~T, ~val, F.opt(T, bad, r)) == Some{n} : Maybe<&2, Nat>}:
25  %Equal.sym(Bool, bad, False{}, hb) : {SF.mval(~T, ~val, F.opt(T, _, r)) == Some{n} : Maybe<&2, Nat>}
26  Equal.cong(Nat, Maybe<&2, Nat>, t => Some{t}, val(r), n, hv)