proposition: Lemma loop_superposing_2 {a b c d e} (ab : C a b) (cd : C (bif e c) (bif e d)) : bimap ab (loop cd) ⩯ loop (assoc_l >>> bimap swap (id_ _) >>> assoc_r >>> bimap ab cd >>> assoc_l >>> bimap swap (id_ _) >>> assoc_r).
proof: Proof. rewrite swap_bimap, loop_superposing. rewrite loop_natural_left, loop_natural_right. rewrite (swap_bimap cd ab). rewrite <- !cat_assoc. rewrite local_rewrite1. rewrite 2 cat_assoc. rewrite <- (cat_assoc swap assoc_r). rewrite local_rewrite2. rewrite <- !cat_assoc. reflexivity. Qed.
imports: Coq(Setoid Morphisms) ITree.Basics(CategoryOps CategoryTheory)