def internal_all_if

bend-mathlib@0.8.1.0 · list.bend:532

import Base

532# Base 2.0.38 short-circuits each through a thunk (List.all.if, List.any.if, List.find.if), so the cons step is proved by cases on the head's test.
533def internal_all_if(b: Bool, -r: Bool) -> {Bool.and(b, r) == List.all.if(u => r, b) : Bool}:
534  match b:
535    case False{}:
536      {==}
537    case True{}:
538      {==}