def internal_all_map

bend-mathlib@0.8.1.0 · list.bend:1493

import Base

1493# Unfolds List.all directly, so its proof depends on Base's definition (PLAN F39).
1494def internal_all_map(~A: Type, ~B: Type, ~f: A -> B, ~p: B -> Bool, xs: List<A>) -> {List.all(~&1, ~B, ~p, List.map(~A, ~B, ~f, xs)) == List.all(~&1, ~A, ~(x => p(f(x))), xs) : Bool}:
1495  match xs:
1496    case Nil{}:
1497      {==}
1498    case h <> t:
1499      %internal_all_map(~A, ~B, ~f, ~p, t) : {List.all.if(u => List.all(~&1, ~B, ~p, List.map(~A, ~B, ~f, t)), p(f(h))) == List.all.if(u => _, p(f(h))) : Bool}
1500      {==}