law all_append

bend-mathlib@0.8.1.0 · list.bend:608

import Base

608# All over an append is all over each part, joined by and.
609law all_append:
610  for ~a: Quant
611  for ~A: Kind(a)
612  for ~f: A -> Bool
613  for xs: List<a, A>
614  for -ys: List<a, A>
615  {List.all(~a, ~A, ~f, List.append(a, A, xs, ys)) == Bool.and(List.all(~a, ~A, ~f, xs), List.all(~a, ~A, ~f, ys)) : Bool}