law mem_append_left

bend-mathlib@0.8.1.0 · list.bend:789

import Base

789# A member of xs is a member of xs ++ ys (Nat lists).
790law mem_append_left:
791  for xs: List<&2, Nat>
792  for ys: List<&2, Nat>
793  for x: Nat
794  for h: mem(~Nat, ~Nat.is_eq, x, xs)
795  mem(~Nat, ~Nat.is_eq, x, List.append(&2, Nat, xs, ys))