proposition: Lemma iter_dinatural_helper: forall (a b c : Type) (f : Kleisli (stateT S M) a (b + c)) (g : Kleisli (stateT S M) b (a + c)), internalize (f >>> case_ g inr_) >>> pure iso ⩯ internalize f >>> pure iso >>> case_ (internalize g >>> pure iso) inr_.
proof: Proof. destruct CM. intros a b c f g. repeat red. destruct a0. unfold cat, Cat_Kleisli, internalize. cbn. repeat rewrite bind_bind. apply Proper_bind. - reflexivity. - repeat red. destruct a1 as [s' [x | y]]. + unfold pure. rewrite bind_ret_l. unfold case_, Case_Kleisli, Function.case_sum. reflexivity. + unfold pure. rewrite bind_ret_l. unfold case_, Case_Kleisli, Function.case_sum. cbn. rewrite bind_ret_l. reflexivity. Qed.
imports: Coq(Setoid Morphisms) ExtLib(Structures.Monad) ITree(Basics.Basics Basics.Category Basics.CategoryKleisli Basics.CategoryKleisliFacts Basics.Monad)