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