def internal_all_filter_put
bend-mathlib@0.8.1.0 · list.bend:1443
import bend-mathlib@0.8.1.0/list.bend as List
import Base
1443def internal_all_filter_put(~A: Data, ~q: A -> Bool, +h: A, r: List<&2, A>, b: Bool) -> {List.all(~&2, ~A, ~q, List.filter.put(A, h, r, b)) == Bool.and(Bool.or(Bool.not(b), q(h)), List.all(~&2, ~A, ~q, r)) : Bool}:
1444 match b:
1445 case False{}:
1446 {==}
1447 case True{}:
1448 Equal.sym(Bool, Bool.and(q(h), List.all(~&2, ~A, ~q, r)), List.all(~&2, ~A, ~q, h <> r), internal_all_cons(~&2, ~A, ~q, h, r))