~/jendhub

def le_witness.lift

minebender-game@1.0.0.0 · proof_base.bend:659

import minebender-game@1.0.0.0/proof_base.bend as ProofBase
import Base

659def le_witness.lift(+p: Nat, +q: Nat, r: LeW(p, q)) -> LeW(1n+p, 1n+q):
660  match r:
661    case (k, e):
662      (k, %Equal.sym(Nat, q, Nat.add(p, k), e) : {1n+_ == 1n+Nat.add(p, k) : Nat}; {==})

Uses (5)

Used by (1)