proposition: Lemma try_catch_ret : forall E Err R r (kcatch : Err -> itree (exceptE Err +' E) R), try_catch (Ret r) kcatch ≅ Ret r.
proof: Proof. intros. unfold try_catch. unfold iter, Iter_Kleisli, Basics.iter, MonadIter_itree. rewrite unfold_iter. cbn. rewrite bind_ret_l. reflexivity. Qed.
imports: Coq(Morphisms) ExtLib(Structures.Monad) Paco(paco) ITree(ITree ITreeFacts Events.Exception)