proposition: Fact local_rewrite1 {a b c}: bimap (id_ a) (swap_ b c) >>> assoc_l >>> swap ⩯ assoc_l >>> bimap swap (id_ c) >>> assoc_r.
proof: Proof. symmetry. apply fwd_eqn; intros h Eq. do 2 apply (cat_eq2_l (bimap (id_ _) swap)) in Eq. rewrite <- cat_assoc, bimap_cat, swap_involutive, cat_id_l, bimap_id, cat_id_l in Eq. rewrite <- (cat_assoc _ _ assoc_r), <- (cat_assoc _ assoc_l _) in Eq. rewrite <- swap_assoc_l in Eq. rewrite (cat_assoc _ _ assoc_r) in Eq. rewrite assoc_l_mono in Eq. rewrite cat_id_r in Eq. rewrite cat_assoc. assumption. Qed.
imports: Coq(Setoid Morphisms) ITree.Basics(CategoryOps CategoryTheory)