law any_reverse_sym

bend-mathlib@0.8.1.0 · list.bend:2823

import Base

2823# Reversing does not change whether some element satisfies a predicate, reversed to rewrite toward the simple side.
2824law any_reverse_sym:
2825  for ~a: Quant
2826  for ~A: Kind(a)
2827  for ~f: A -> Bool
2828  for xs: List<a, A>
2829  {List.any(~a, ~A, ~f, xs) == List.any(~a, ~A, ~f, List.reverse(a, A, xs)) : Bool}