def pd.nd

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

import Base

75def pd.nd(+p: Nat, h: {1n+p == 0n : Nat}) -> Empty:
76  %h : pd.ndisc(_)
77  Unit{}