def ud.p1

bend-osdev-u32@0.1.0.0 · PROOF.bend:1823

import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOF

import Base

1823def ud.p1(-x: Nat, -y: Nat, -c: Nat, -d: Nat, pr: {x == y : Nat} & {Nat.is_lt(c, d) == True{} : Bool}) -> {x == y : Nat}:
1824  (+a, +b) = pr
1825  a

Uses (5)

Used by (2)