law all_append_sym

bend-mathlib@0.8.1.0 · list.bend:2494

import Base

2494# All over an append is all over each part, joined by and, reversed to rewrite toward the simple side.
2495law all_append_sym:
2496  for ~a: Quant
2497  for ~A: Kind(a)
2498  for ~f: A -> Bool
2499  for xs: List<a, A>
2500  for -ys: List<a, A>
2501  {Bool.and(List.all(~a, ~A, ~f, xs), List.all(~a, ~A, ~f, ys)) == List.all(~a, ~A, ~f, List.append(a, A, xs, ys)) : Bool}