def wd.p2
import bend-osdev-word64@0.1.1.0/PROOF_div.bend as PROOFDivimport Base
155def wd.p2(-x: Nat, -y: Nat, -c: Nat, -d: Nat, pr: {x == y : Nat} & {Nat.is_lt(c, d) == True{} : Bool}) -> {Nat.is_lt(c, d) == True{} : Bool}:
156 (+u, +v) = pr
157 v