def bits.sub_refl

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

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

166def bits.sub_refl(+n: Nat, +x: Word(n)) -> {C.CapBits.subset(n, x, x) == True{} : Bool}:
167  match n:
168    case 0n:
169      {==}
170    case 1n+n1:
171      match x:
172        case WCon{True{}, +xt}:
173          bits.sub_refl(n1, xt)
174        case WCon{False{}, +xt}:
175          bits.sub_refl(n1, xt)