def internal_find_put_or

bend-mathlib@0.8.1.0 · list.bend:1996

import Base

1996def internal_find_put_or(-A: Data, h: A, r: Maybe<&2, A>, -s: Maybe<&2, A>, b: Bool) -> {Maybe.or(&2, A, internal_find_put(A, h, r, b), s) == internal_find_put(A, h, Maybe.or(&2, A, r, s), b) : Maybe<&2, A>}:
1997  match b:
1998    case False{}:
1999      {==}
2000    case True{}:
2001      {==}