proposition: Theorem source_distributes : forall {M : Type -> Type} `{Monad M} {R A} (m : EitherT R M A) (f : A -> EitherT R M A), source (fun (r : R) (yield : R -> A -> EitherT R M R) => m >>= yield r) >>= (fun x : A => source (fun (r : R) (yield : R -> A -> EitherT R M R) => f x >>= yield r)) = source (fun (r : R) (yield : R -> A -> EitherT R M R) => m >>= f >>= yield r).
proof: Proof. Admitted. #[export] Instance Source_MonadTrans {M : Type -> Type} `{Monad M} {R} : @MonadTrans (fun N => Source N R) M _ Source_Monad := { lift := fun _ m => source (fun r yield => lift m >>= yield r) }. Proof. - intros. unfold source. simpl pure. extensionality e. unfold compose at 1. f_equal. f_equal. unfold flip. unfold compose at 1. unfold bind. rewrite trans_law_1_x. pose proof app_fmap_compose_x. specialize (H0 (EitherT R M) is_applicative A (EitherT R M R)). simpl join. simpl pure. simpl pure in H0. extensionality p. extensionality q. rewrite <- H0. pose proof monad_law_3_x. specialize (H1 (EitherT R M) EitherT_Monad R (p e q)). simpl join in H1. simpl pure in H1. assumption. - intros. pose (@trans_law_2 (EitherT R) M _ _ _ A). unfold compose. rewrite e. rewrite source_distributes. reflexivity. Defined.
imports: Cont EitherT Trans