def wn.le_rw

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

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

import Base

103def wn.le_rw(-x: Nat, -x2: Nat, -y: Nat, e: {x == x2 : Nat}, h: {Nat.is_le(x, y) == True{} : Bool}) -> {Nat.is_le(x2, y) == True{} : Bool}:
104  %e : {Nat.is_le(_, y) == True{} : Bool}
105  h

Uses (3)

Used by (3)