def wn.lt_irrefl

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

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

import Base

149def wn.lt_irrefl(x: Nat, h: {Nat.is_lt(x, x) == True{} : Bool}) -> Empty:
150  match x:
151    case 0n:
152      wn.ft(h)
153    case 1n+p:
154      wn.lt_irrefl(p, h)

Uses (5)

Used by (6)