law any_append

bend-mathlib@0.8.1.0 · list.bend:624

import Base

624# Any over an append is any over each part, joined by or.
625law any_append:
626  for ~a: Quant
627  for ~A: Kind(a)
628  for ~f: A -> Bool
629  for xs: List<a, A>
630  for -ys: List<a, A>
631  {List.any(~a, ~A, ~f, List.append(a, A, xs, ys)) == Bool.or(List.any(~a, ~A, ~f, xs), List.any(~a, ~A, ~f, ys)) : Bool}