proposition: Lemma case_l' {A B: Type} (f: Kleisli m (void + A) (void + B)) : unit_l' >>> f ⩯ fun a => f (inr a).
proof: Proof. rewrite unit_l'_pure. intro. unfold cat, Cat_Kleisli, pure. 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)