def wn.le_rw2

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

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

import Base

145def wn.le_rw2(-x: Nat, -y: Nat, -y2: Nat, e: {y == y2 : Nat}, h: {Nat.is_le(x, y) == True{} : Bool}) -> {Nat.is_le(x, y2) == True{} : Bool}:
146  %e : {Nat.is_le(x, _) == True{} : Bool}
147  h

Uses (3)

Used by (6)