PROOF.rb_eq: def of bend-osdev-gf@0.1.1.0
Import: import bend-osdev-gf@0.1.1.0/PROOF.bend as PROOF
Lines 302-311 of bend-osdev-gf@0.1.1.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&start_line=302&end_line=311

import Base
import bend-osdev-gf@0.1.1.0/gf.bend as G

def rb_eq(-a0: Bool, -a1: Bool, -a2: Bool, -a3: Bool, -a4: Bool, -a5: Bool, -a6: Bool, -a7: Bool, -c0: Bool, -c1: Bool, -c2: Bool, -c3: Bool, -c4: Bool, -c5: Bool, -c6: Bool, -c7: Bool, e0: {a0 == c0 : Bool}, e1: {a1 == c1 : Bool}, e2: {a2 == c2 : Bool}, e3: {a3 == c3 : Bool}, e4: {a4 == c4 : Bool}, e5: {a5 == c5 : Bool}, e6: {a6 == c6 : Bool}, e7: {a7 == c7 : Bool}) -> {G.Gf8Bits{a0, a1, a2, a3, a4, a5, a6, a7} == G.Gf8Bits{c0, c1, c2, c3, c4, c5, c6, c7} : G.Gf8Bits}:
  %e0 : {G.Gf8Bits{a0, a1, a2, a3, a4, a5, a6, a7} == G.Gf8Bits{_, c1, c2, c3, c4, c5, c6, c7} : G.Gf8Bits}
  %e1 : {G.Gf8Bits{a0, a1, a2, a3, a4, a5, a6, a7} == G.Gf8Bits{a0, _, c2, c3, c4, c5, c6, c7} : G.Gf8Bits}
  %e2 : {G.Gf8Bits{a0, a1, a2, a3, a4, a5, a6, a7} == G.Gf8Bits{a0, a1, _, c3, c4, c5, c6, c7} : G.Gf8Bits}
  %e3 : {G.Gf8Bits{a0, a1, a2, a3, a4, a5, a6, a7} == G.Gf8Bits{a0, a1, a2, _, c4, c5, c6, c7} : G.Gf8Bits}
  %e4 : {G.Gf8Bits{a0, a1, a2, a3, a4, a5, a6, a7} == G.Gf8Bits{a0, a1, a2, a3, _, c5, c6, c7} : G.Gf8Bits}
  %e5 : {G.Gf8Bits{a0, a1, a2, a3, a4, a5, a6, a7} == G.Gf8Bits{a0, a1, a2, a3, a4, _, c6, c7} : G.Gf8Bits}
  %e6 : {G.Gf8Bits{a0, a1, a2, a3, a4, a5, a6, a7} == G.Gf8Bits{a0, a1, a2, a3, a4, a5, _, c7} : G.Gf8Bits}
  %e7 : {G.Gf8Bits{a0, a1, a2, a3, a4, a5, a6, a7} == G.Gf8Bits{a0, a1, a2, a3, a4, a5, a6, _} : G.Gf8Bits}
  {==}

Uses (2):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/gf.bend&name=Gf8Bits