proposition: Lemma unit_l_pure (A : Type) : unit_l ⩯ @pure _ _ (void + A) A unit_l.
proof: Proof. intros [[]|]. reflexivity. Qed.
imports: Coq(Program Setoid Morphisms RelationClasses) ExtLib(Structures.Monad) ITree(Basics.Basics Basics.Category Basics.Monad Basics.CategoryFunctor Basics.CategoryKleisli Basics.Function)