proposition: Lemma pure_assoc_l {a b c : Type} : assoc_l (C := Kleisli m) (bif := sum) ⩯ pure (m := m) (a := a + (b + c))%type assoc_l.
proof: Proof. cbv; intros x; destruct x as [ | []]; try setoid_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)