module Data.Maybe.Properties export mapFusion : (s : Maybe a) -> (f . g) <$> s = f <$> [| g s |] mapFusion Nothing = Refl mapFusion (Just x) = Refl