def pd.nil

bend-osdev-cbc@0.1.0.0 · PROOF_padded.bend:86

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B

86def pd.nil(xs: List<&2, U32>) -> {B.len(xs) == 0n : Nat} -> {xs == Nil{} : List<&2, U32>}:
87  match xs:
88    case Nil{}:
89      h => {==}
90    case Con{x, t}:
91      h => Empty.absurd({Con{x, t} == Nil{} : List<&2, U32>}, pd.nd(B.len(t), h))