def fst_bump2

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/nat.bend:506

import Base

506def fst_bump2(p: Nat & Nat) -> {Pair.fst(Nat, Nat, bump2(p)) == 1n+Pair.fst(Nat, Nat, p) : Nat}:
507  (q, r) = p
508  {==}