def eq_sh2

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqa.bend:93

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C

93def eq_sh2(+j: Nat, +a: Nat, +b: Nat) -> {Nat.is_eq(C.shift(j, C.shift(j, a)), C.shift(j, C.shift(j, b))) == Nat.is_eq(a, b) : Bool}:
94  Equal.trans(Bool, Nat.is_eq(C.shift(j, C.shift(j, a)), C.shift(j, C.shift(j, b))), Nat.is_eq(C.shift(j, a), C.shift(j, b)), Nat.is_eq(a, b), eq_sh(j, C.shift(j, a), C.shift(j, b)), eq_sh(j, a, b))