def internal_filter_put_append

bend-mathlib@0.8.1.0 · list.bend:640

import Base

640def internal_filter_put_append(-A: Data, h: A, r: List<&2, A>, s: List<&2, A>, b: Bool) -> {List.append(&2, A, List.filter.put(A, h, r, b), s) == List.filter.put(A, h, List.append(&2, A, r, s), b) : List<&2, A>}:
641  match b:
642    case False{}:
643      {==}
644    case True{}:
645      {==}