def wn.lt_rw2

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

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

import Base

99def wn.lt_rw2(-x: Nat, -y: Nat, -y2: Nat, e: {y == y2 : Nat}, h: {Nat.is_lt(x, y) == True{} : Bool}) -> {Nat.is_lt(x, y2) == True{} : Bool}:
100  %e : {Nat.is_lt(x, _) == True{} : Bool}
101  h

Uses (3)

Used by (10)