law any_append_sym

bend-mathlib@0.8.1.0 · list.bend:2506

import Base

2506# Any over an append is any over each part, joined by or, reversed to rewrite toward the simple side.
2507law any_append_sym:
2508  for ~a: Quant
2509  for ~A: Kind(a)
2510  for ~f: A -> Bool
2511  for xs: List<a, A>
2512  for -ys: List<a, A>
2513  {Bool.or(List.any(~a, ~A, ~f, xs), List.any(~a, ~A, ~f, ys)) == List.any(~a, ~A, ~f, List.append(a, A, xs, ys)) : Bool}