~/jendhub

def un.dmu.s

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

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

1071def un.dmu.s(-s: Nat, -t: Nat, -r1: Nat, -r2: Nat, pr: {s == t : Nat} & {r1 == r2 : Nat}) -> {1n+s == 1n+t : Nat} & {r1 == r2 : Nat}:
1072  (a, c) = pr
1073  (un.succ_cong(s, t, a), c)

Uses (4)

Used by (1)