def set.eq_intro

bend-osdev-caps@0.1.0.0 · PROOF.bend:157

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

157# two sets are equal when their parts are
158def 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()}:
159  %e1 : {C.CapSetW{U32{l1}, h1} == C.CapSetW{U32{_}, h2} : C.CapSet()}
160  %e2 : {C.CapSetW{U32{l1}, h1} == C.CapSetW{U32{l1}, _} : C.CapSet()}
161  {==}