F64addf.rc2: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addf.bend as F64addf
Lines 92-95 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addf.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addf.bend&start_line=92&end_line=95

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L

def rc2(+s: Bool, +s2: Bool, +hs: {s == s2 : Bool}, +m: Nat, +m2: Nat, +hm: {m == m2 : Nat}, +x: Nat, +x2: Nat, +hx: {x == x2 : Nat}) -> {SF.round(s, m, x) == SF.round(s2, m2, x2) : F.F64}:
  +e1 = L.subst(Bool, z => {SF.round(s, m, x) == SF.round(z, m, x) : F.F64}, s, s2, hs, {==})
  +e2 = L.subst(Nat, z => {SF.round(s, m, x) == SF.round(s2, z, x) : F.F64}, m, m2, hm, e1)
  L.subst(Nat, z => {SF.round(s, m, x) == SF.round(s2, m2, z) : F.F64}, x, x2, hx, e2)

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend&name=subst
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=round
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=F64