~/jendhub

def AP.lt_rw_k

bend-osdev-array@0.1.0.1 · PROOF.bend:1702

import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF
import Base

1702def AP.lt_rw_k(-k: Nat, -x: Nat, -s: Nat, e: {k == x : Nat}, h: {Nat.is_lt(k, s) == True{} : Bool}) -> {Nat.is_lt(x, s) == True{} : Bool}:
1703  %e : {Nat.is_lt(_, s) == True{} : Bool}
1704  h

Uses (3)

Used by (1)