law maybe_bind_map_sym

bend-mathlib@0.8.1.0 · maybe.bend:366

import Base

366# Binding after a map binds the composition, reversed to rewrite toward the simple side.
367law maybe_bind_map_sym:
368  for ~A: Data
369  for ~B: Data
370  for ~C: Data
371  for ~f: A -> B
372  for ~g: B -> Maybe<&2, C>
373  for m: Maybe<&2, A>
374  {Maybe.bind(&2, A, C, m, x => g(f(x))) == Maybe.bind(&2, B, C, Maybe.map(&2, A, B, f, m), g) : Maybe<&2, C>}