~/jendhub

law mem_cons_of_mem

bend-mathlib@0.8.1.0 · list.bend:767

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

767# A member of a Nat list stays a member when a head is prepended.
768law mem_cons_of_mem:
769  for x: Nat
770  for y: Nat
771  for -xs: List<&2, Nat>
772  for h: mem(~Nat, ~Nat.is_eq, x, xs)
773  mem(~Nat, ~Nat.is_eq, x, y <> xs)

Uses (8)

Used by (1)