proposition: Lemma loop_superposing {a b c d e} (ab : C (bif e a) (bif e b)) (cd : C c d) : bimap (loop ab) cd ⩯ loop (assoc_l >>> bimap ab cd >>> assoc_r).
proof: Proof. unfold loop. cat_auto. - transitivity ( inr_ >>> iter ( (inl_ >>> assoc_r >>> inl_) >>> case_ (assoc_l >>> bimap ab cd >>> assoc_r >>> bimap inl_ (id_ _)) inr_)). + rewrite cat_assoc, iter_natural. do 2 (cat_auto_step; cat_auto). + rewrite iter_dinatural. do 3 (cat_auto; cat_auto_step). - rewrite iter_unfold. cat_auto. Qed.
imports: Coq(Setoid Morphisms) ITree.Basics(CategoryOps CategoryTheory)