law find_append

bend-mathlib@0.8.1.0 · list.bend:2003

import Base

2003# Finding in an append finds in the first part, or else in the second.
2004law find_append:
2005  for ~A: Data
2006  for ~f: A -> Bool
2007  for xs: List<&2, A>
2008  for ys: List<&2, A>
2009  {List.find(~A, ~f, List.append(&2, A, xs, ys)) == Maybe.or(&2, A, List.find(~A, ~f, xs), List.find(~A, ~f, ys)) : Maybe<&2, A>}