law contains_append_sym

bend-mathlib@0.8.1.0 · list.bend:2529

import Base

2529# An append contains x iff either part does, reversed to rewrite toward the simple side.
2530law contains_append_sym:
2531  for ~A: Data
2532  for ~eq: A -> A -> Bool
2533  for xs: List<&2, A>
2534  for -ys: List<&2, A>
2535  for +x: A
2536  {Bool.or(List.contains(~A, ~eq, xs, x), List.contains(~A, ~eq, ys, x)) == List.contains(~A, ~eq, List.append(&2, A, xs, ys), x) : Bool}