F64close.or3: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64close.bend as F64close
Lines 22-28 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64close.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64close.bend&start_line=22&end_line=28

import Base

# three-way disjunction congruence over abstract Booleans (book-less: the
# checker never unfolds the comparisons it is applied to)
def or3(+x1: Bool, +x2: Bool, +x3: Bool, +y1: Bool, +y2: Bool, +y3: Bool, +h1: {x1 == y1 : Bool}, +h2: {x2 == y2 : Bool}, +h3: {x3 == y3 : Bool}) -> {Bool.or(Bool.or(x1, x2), x3) == Bool.or(Bool.or(y1, y2), y3) : Bool}:
  +c1 = Equal.cong(Bool, Bool, t => Bool.or(Bool.or(t, x2), x3), x1, y1, h1)
  +c2 = Equal.cong(Bool, Bool, t => Bool.or(Bool.or(y1, t), x3), x2, y2, h2)
  +c3 = Equal.cong(Bool, Bool, t => Bool.or(Bool.or(y1, y2), t), x3, y3, h3)
  Equal.trans(Bool, Bool.or(Bool.or(x1, x2), x3), Bool.or(Bool.or(y1, x2), x3), Bool.or(Bool.or(y1, y2), y3), c1, Equal.trans(Bool, Bool.or(Bool.or(y1, x2), x3), Bool.or(Bool.or(y1, y2), x3), Bool.or(Bool.or(y1, y2), y3), c2, c3))

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  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