proposition: Lemma pure_swap {A B}: @pure _ _ (A+B) _ swap ⩯ swap.
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)