fact: Definition Source_apply {M : Type -> Type} `{Applicative M} {R X Y} (f : Source M R (X -> Y)) (x : Source M R X) : Source M R Y := match f with Source_ k => match x with Source_ j => Source_ M R Y (ap k j) end end.
imports: Cont EitherT Trans