proposition: Lemma loop_dinatural' {a b c d} (cd : C c d) (dc: C d c) (ab_: C (bif c a) (bif c b)) : (cd >>> dc) ⩯ id_ _ -> loop (bimap dc (id_ _) >>> ab_ >>> bimap cd (id_ _)) ⩯ loop ab_.
proof: Proof. intros Hij. rewrite loop_dinatural. rewrite <- cat_assoc. rewrite bimap_cat. rewrite Hij. rewrite cat_id_l. rewrite bimap_id. rewrite cat_id_l. reflexivity. Qed.
imports: Coq(Setoid Morphisms) ITree.Basics(CategoryOps CategoryTheory)