def internal_all_cons_test

bend-mathlib@0.8.1.0 · list.bend:566

import Base

566# The cons case of all with the head's test given as a value, for a head that cannot be used twice (a pair under a predicate that reads both parts).
567def internal_all_cons_test(~a: Quant, ~A: Kind(a), ~f: A -> Bool, -h: A, -t: List<a, A>, b: Bool, e: {f(h) == b : Bool}) -> {Bool.and(b, List.all(~a, ~A, ~f, t)) == List.all(~a, ~A, ~f, h <> t) : Bool}:
568  %Equal.sym(Bool, f(h), b, e) : {Bool.and(b, List.all(~a, ~A, ~f, t)) == List.all.if(u => List.all(~a, ~A, ~f, t), _) : Bool}
569  internal_all_if(b, List.all(~a, ~A, ~f, t))