proposition: Lemma case_l {A B: Type} (ab: Kleisli m A (void + B)) : ab >>> unit_l ⩯ map unit_l ab.
proof: Proof. rewrite unit_l_pure. reflexivity. Qed.
imports: Coq(Program Setoid Morphisms RelationClasses) ExtLib(Structures.Monad) ITree(Basics.Basics Basics.Category Basics.Monad Basics.CategoryFunctor Basics.CategoryKleisli Basics.Function)