proposition: Lemma case_r' {A B: Type} (f: Kleisli m (A + void) (B + void)) : unit_r' >>> f ⩯ fun a => f (inl a).
proof: Proof. rewrite unit_r'_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)