law maybe_bind_assoc_sym

bend-mathlib@0.8.1.0 · maybe.bend:245

import Base

245# Bind is associative, reversed to rewrite toward the simple side.
246law maybe_bind_assoc_sym:
247  for ~A: Data
248  for ~B: Data
249  for ~C: Data
250  for -f: A -> Maybe<&2, B>
251  for -g: B -> Maybe<&2, C>
252  for m: Maybe<&2, A>
253  {Maybe.bind(&2, A, C, m, x => Maybe.bind(&2, B, C, f(x), g)) == Maybe.bind(&2, B, C, Maybe.bind(&2, A, B, m, f), g) : Maybe<&2, C>}