F64mulv.mswap: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mulv.bend as F64mulv
Lines 34-35 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mulv.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mulv.bend&start_line=34&end_line=35

import Base
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/math/typed/f64mulc.bend as MC

def mswap(+s1: Bool, +s2: Bool, +hs: {s1 == s2 : Bool}, +r1: F.F64, +r2: F.F64, +hr: {r1 == r2 : F.F64}, +p1: Bool, +q1: Bool, +h0: {p1 == q1 : Bool}, +p2: Bool, +q2: Bool, +h1: {p2 == q2 : Bool}, +p3: Bool, +q3: Bool, +h2: {p3 == q3 : Bool}, +p4: Bool, +q4: Bool, +h3: {p4 == q4 : Bool}, +p5: Bool, +q5: Bool, +h4: {p5 == q5 : Bool}, +p6: Bool, +q6: Bool, +h5: {p6 == q6 : Bool}) -> {MC.mimpl(s1, p1, p2, p3, p4, p5, p6, r1) == MC.mimpl(s2, q1, q2, q3, q4, q5, q6, r2) : F.F64}:
  Equal.trans(F.F64, MC.mimpl(s1, p1, p2, p3, p4, p5, p6, r1), MC.mimpl(s2, p1, p2, p3, p4, p5, p6, r1), MC.mimpl(s2, q1, q2, q3, q4, q5, q6, r2), Equal.cong(Bool, F.F64, w => MC.mimpl(w, p1, p2, p3, p4, p5, p6, r1), s1, s2, hs), Equal.trans(F.F64, MC.mimpl(s2, p1, p2, p3, p4, p5, p6, r1), MC.mimpl(s2, p1, p2, p3, p4, p5, p6, r2), MC.mimpl(s2, q1, q2, q3, q4, q5, q6, r2), Equal.cong(F.F64, F.F64, w => MC.mimpl(s2, p1, p2, p3, p4, p5, p6, w), r1, r2, hr), Equal.trans(F.F64, MC.mimpl(s2, p1, p2, p3, p4, p5, p6, r2), MC.mimpl(s2, q1, p2, p3, p4, p5, p6, r2), MC.mimpl(s2, q1, q2, q3, q4, q5, q6, r2), Equal.cong(Bool, F.F64, w => MC.mimpl(s2, w, p2, p3, p4, p5, p6, r2), p1, q1, h0), Equal.trans(F.F64, MC.mimpl(s2, q1, p2, p3, p4, p5, p6, r2), MC.mimpl(s2, q1, q2, p3, p4, p5, p6, r2), MC.mimpl(s2, q1, q2, q3, q4, q5, q6, r2), Equal.cong(Bool, F.F64, w => MC.mimpl(s2, q1, w, p3, p4, p5, p6, r2), p2, q2, h1), Equal.trans(F.F64, MC.mimpl(s2, q1, q2, p3, p4, p5, p6, r2), MC.mimpl(s2, q1, q2, q3, p4, p5, p6, r2), MC.mimpl(s2, q1, q2, q3, q4, q5, q6, r2), Equal.cong(Bool, F.F64, w => MC.mimpl(s2, q1, q2, w, p4, p5, p6, r2), p3, q3, h2), Equal.trans(F.F64, MC.mimpl(s2, q1, q2, q3, p4, p5, p6, r2), MC.mimpl(s2, q1, q2, q3, q4, p5, p6, r2), MC.mimpl(s2, q1, q2, q3, q4, q5, q6, r2), Equal.cong(Bool, F.F64, w => MC.mimpl(s2, q1, q2, q3, w, p5, p6, r2), p4, q4, h3), Equal.trans(F.F64, MC.mimpl(s2, q1, q2, q3, q4, p5, p6, r2), MC.mimpl(s2, q1, q2, q3, q4, q5, p6, r2), MC.mimpl(s2, q1, q2, q3, q4, q5, q6, r2), Equal.cong(Bool, F.F64, w => MC.mimpl(s2, q1, q2, q3, q4, w, p6, r2), p5, q5, h4), Equal.cong(Bool, F.F64, w => MC.mimpl(s2, q1, q2, q3, q4, q5, w, r2), p6, q6, h5))))))))

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=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mulc.bend&name=mimpl
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=F64