law contains_reverse_sym

bend-mathlib@0.8.1.0 · list.bend:2834

import Base

2834# Reversing does not change whether a list contains x, reversed to rewrite toward the simple side.
2835law contains_reverse_sym:
2836  for ~A: Data
2837  for ~eq: A -> A -> Bool
2838  for xs: List<&2, A>
2839  for +x: A
2840  {List.contains(~A, ~eq, xs, x) == List.contains(~A, ~eq, List.reverse(&2, A, xs), x) : Bool}