def AP.lt_rw_r

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

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

import Base

1006def AP.lt_rw_r(-k: Nat, -x: Nat, -y: Nat, e: {x == y : Nat}, h: {Nat.is_lt(k, y) == True{} : Bool}) -> {Nat.is_lt(k, x) == True{} : Bool}:
1007  %Equal.sym(Nat, x, y, e) : {Nat.is_lt(k, _) == True{} : Bool}
1008  h

Uses (4)

Used by (2)