def internal_all_cons

bend-mathlib@0.8.1.0 · list.bend:562

import Base

562# The cons case of all, any, find and contains as lemmas, so a change to their Base definitions stays in one place (PLAN F39).
563def internal_all_cons(~a: Quant, ~A: Kind(a), ~f: A -> Bool, h: A, -t: List<a, A>) -> {Bool.and(f(h), List.all(~a, ~A, ~f, t)) == List.all(~a, ~A, ~f, h <> t) : Bool}:
564  internal_all_if(f(h), List.all(~a, ~A, ~f, t))