def internal_or_of_or

bend-mathlib@0.8.1.0 · list.bend:718

import Base

718def internal_or_of_or(a: Bool, -b: Bool, -c: Bool, h: {Bool.or(a, b) == True{} : Bool}, k: {b == True{} : Bool} -> {c == True{} : Bool}) -> {Bool.or(a, c) == True{} : Bool}:
719  match a:
720    case False{}:
721      k(h)
722    case True{}:
723      {==}