[Agda] Maybe-like combinator for propositions

[Dr. ERDI Gergo]

Hi,

I needed the following definition for something I've been playing around 
with:

   data Partial {A : Set} (P : A → Set) (Q : Set) : Maybe A → Set where
     Just : ∀ {x} → P x → Partial P Q (just x)
     Nothing : Q → Partial P Q nothing

   Partial-Just : ∀ {A P Q x} → Partial {A} P Q (just x) → P x
   Partial-Just (Just P) = P

   Partial-Nothing : ∀ {A P Q} → Partial {A} P Q nothing → Q
   Partial-Nothing (Nothing Q) = Q

Apart from the horrible name, this sounds very basic. I have this feeling 
something like this should already be in the standard library (possibly 
some combination of `maybe` and `All` from `Data.Maybe`?). Is there a 
nicer way (and a nicer name!) to do this?

Thanks,
 	Gergo

-- 

   .--= ULLA! =-----------------.
    \     http://gergo.erdi.hu   \
     `---= gergo at erdi.hu =-------'
Speak the truth, but leave immediately after.