def wn.lt_rw

bend-osdev-word64@0.1.1.0 · proof_value.bend:95

import bend-osdev-word64@0.1.1.0/proof_value.bend as ProofValue

import Base

95def wn.lt_rw(-x: Nat, -x2: Nat, -y: Nat, e: {x == x2 : Nat}, h: {Nat.is_lt(x, y) == True{} : Bool}) -> {Nat.is_lt(x2, y) == True{} : Bool}:
96  %e : {Nat.is_lt(_, y) == True{} : Bool}
97  h

Uses (3)

Used by (5)