PROOF.set.eq_intro: def of bend-osdev-caps@0.1.0.0
Import: import bend-osdev-caps@0.1.0.0/PROOF.bend as PROOF
Lines 157-161 of bend-osdev-caps@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&start_line=157&end_line=161

import Base
import bend-osdev-caps@0.1.0.0/caps.bend as C

# two sets are equal when their parts are
def set.eq_intro(+l1: Word(32n), +l2: Word(32n), +h1: Word(9n), +h2: Word(9n), +e1: {l1 == l2 : Word(32n)}, +e2: {h1 == h2 : Word(9n)}) -> {C.CapSetW{U32{l1}, h1} == C.CapSetW{U32{l2}, h2} : C.CapSet()}:
  %e1 : {C.CapSetW{U32{l1}, h1} == C.CapSetW{U32{_}, h2} : C.CapSet()}
  %e2 : {C.CapSetW{U32{l1}, h1} == C.CapSetW{U32{l1}, _} : C.CapSet()}
  {==}

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/caps.bend&name=CapSet
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/caps.bend&name=CapSetW