def internal_any_filter_put
bend-mathlib@0.8.1.0 · list.bend:1468
import bend-mathlib@0.8.1.0/list.bend as List
import Base
1468def internal_any_filter_put(~A: Data, ~q: A -> Bool, +h: A, r: List<&2, A>, b: Bool) -> {List.any(~&2, ~A, ~q, List.filter.put(A, h, r, b)) == Bool.or(Bool.and(b, q(h)), List.any(~&2, ~A, ~q, r)) : Bool}:
1469 match b:
1470 case False{}:
1471 {==}
1472 case True{}:
1473 Equal.sym(Bool, Bool.or(q(h), List.any(~&2, ~A, ~q, r)), List.any(~&2, ~A, ~q, h <> r), internal_any_cons(~&2, ~A, ~q, h, r))