def internal_all_if_and

bend-mathlib@0.8.1.0 · list.bend:584

import Base

584# The cons step of all_append, any_append and contains_append, given the step for the tail; proved by cases on the head's test.
585def internal_all_if_and(b: Bool, -r: Bool, -s: Bool, -l: Bool, ih: {l == Bool.and(r, s) : Bool}) -> {List.all.if(u => l, b) == Bool.and(List.all.if(u => r, b), s) : Bool}:
586  match b:
587    case False{}:
588      {==}
589    case True{}:
590      ih