def AP.wh0
bend-osdev-array@0.1.0.1 · PROOF.bend:1663
import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF
import Base
1663def AP.wh0(b: Bool, -s: Nat, -k: Nat, e: {AP.bv(b, 0n) == Nat.add(Nat.double(1n+s), k) : Nat}) -> Empty:
1664 match b:
1665 case False{}:
1666 AP.sz(1n+Nat.add(Nat.double(s), k), Equal.sym(Nat, 0n, 2n+Nat.add(Nat.double(s), k), e))
1667 case True{}:
1668 AP.sz(Nat.add(Nat.double(s), k), Equal.sym(Nat, 0n, 1n+Nat.add(Nat.double(s), k), AP.pred_cong(0n, 1n+Nat.add(Nat.double(s), k), e)))