~/jendhub

law mem_cons_self

bend-mathlib@0.8.1.0 · list.bend:755

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

755# The head of a Nat list is a member of it (membership by Nat.is_eq).
756law mem_cons_self:
757  for x: Nat
758  for -xs: List<&2, Nat>
759  mem(~Nat, ~Nat.is_eq, x, x <> xs)

Uses (10)

Used by (1)