proposition: Lemma map_inr_case_kleisli: forall (a2 b1 b2 c1 c2 : Type) (f2 : Kleisli m a2 b2) (g1 : Kleisli m b1 c1) (g2 : Kleisli m b2 c2), map inr f2 >>> case_ (map inl g1) (map inr g2) ⩯ map inr (f2 >>> g2).
proof: Proof. intros a2 b1 b2 c1 c2 f2 g1 g2. unfold cat, Cat_Kleisli, case_, Case_Kleisli, case_sum. unfold map. unfold cat, Cat_Kleisli. setoid_rewrite bind_bind. unfold pure. setoid_rewrite bind_ret_l. reflexivity. Qed.
imports: Coq(Program Setoid Morphisms RelationClasses) ExtLib(Structures.Monad) ITree(Basics.Basics Basics.Category Basics.Monad Basics.CategoryFunctor Basics.CategoryKleisli Basics.Function)