module Data.Maybe.Properties

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

export
appNothingRight : (0 f : a -> b) -> (y : Maybe a) -> Just f <*> y = Nothing -> y = Nothing
appNothingRight f Nothing prf = Refl