def sp.absurd_tail

bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:152

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M

152def sp.absurd_tail(p: Nat, xs: List<&2, U32>, h: {1n+p == 0n : Nat}) -> {M.cm.split.tail(M.cm.split(B.mask(xs))) == Nil{} : List<&2, U32>}:
153  Empty.absurd({M.cm.split.tail(M.cm.split(B.mask(xs))) == Nil{} : List<&2, U32>}, sp.absurd(p, h))