proposition: Lemma try_catch_throw_prefix_nop : forall E Err R kcatch (ttry : itree (exceptE Err +' E) R), try_catch (throw_prefix ttry) kcatch ≈ throw_prefix ttry.
proof: Proof. intros E Err R kcatch. ginit. gcofix CIH. intros. destruct (observe ttry) eqn : Heq; symmetry in Heq; apply simpobs in Heq. - rewrite Heq. rewrite throw_prefix_ret. rewrite try_catch_ret. gfinal. right. pfold; constructor; auto. - rewrite Heq. rewrite throw_prefix_tau. rewrite try_catch_tau. gstep. constructor. gfinal; left; auto. - destruct e. + destruct e. rewrite Heq. rewrite throw_prefix_exc. rewrite try_catch_ret. gfinal. right. pfold; constructor; auto. + rewrite Heq. rewrite throw_prefix_ev. rewrite try_catch_ev. gstep. constructor. intros. red. rewrite try_catch_tau. repeat rewrite tau_euttge. gfinal. left. auto. Qed.
imports: Coq(Morphisms) ExtLib(Structures.Monad) Paco(paco) ITree(ITree ITreeFacts Events.Exception)