proposition: Lemma try_catch_ev : forall E A Err R (ev: E A) k (kcatch : Err -> itree (exceptE Err +' E) R), try_catch (Vis (inr1 ev) k ) kcatch ≅ Vis (inr1 ev) (fun x => Tau (try_catch (k x) kcatch) ).
proof: Proof. intros. unfold try_catch. unfold iter, Iter_Kleisli, Basics.iter, MonadIter_itree. rewrite unfold_iter. cbn. unfold ITree.map at 3. setoid_rewrite bind_bind. rewrite bind_trigger. cbn. setoid_rewrite bind_ret_l. reflexivity. Qed.
imports: Coq(Morphisms) ExtLib(Structures.Monad) Paco(paco) ITree(ITree ITreeFacts Events.Exception)