~/jendhub

law not_mem_nil

bend-mathlib@0.8.1.0 · list.bend:781

import bend-mathlib@0.8.1.0/list.bend as List
import Base

781# No Nat is a member of the empty list.
782law not_mem_nil:
783  for -x: Nat
784  mem(~Nat, ~Nat.is_eq, x, Nil{}) -> Empty

Uses (6)

Used by (0)

No other definition uses this definition.