Maybe.agda

module Haskell.Law.Maybe where

open import Haskell.Prim
open import Haskell.Prim.Maybe

open import Haskell.Law.Def

Just-injective : Injective (Just {a = a})
Just-injective refl = refl