def internal_reverse_filter_put
bend-mathlib@0.8.1.0 · list.bend:1900
import bend-mathlib@0.8.1.0/list.bend as List
import Base
1900def internal_reverse_filter_put(-A: Data, -h: A, r: List<&2, A>, b: Bool) -> {List.append(&2, A, List.reverse(&2, A, r), List.filter.put(A, h, Nil{}, b)) == List.reverse(&2, A, List.filter.put(A, h, r, b)) : List<&2, A>}:
1901 match b:
1902 case False{}:
1903 append_nil(&2, A, List.reverse(&2, A, r))
1904 case True{}:
1905 Equal.sym(List<&2, A>, List.reverse.go(&2, A, r, [h]), List.append(&2, A, List.reverse(&2, A, r), [h]), reverse_go_spec(&2, A, r, [h]))