proposition: Lemma unfold_interp_fail {E F R} (f : E ~> failT (itree F)) (t : itree E R) : interp_fail f t ≅ (_interp_fail f (observe t)).
proof: Proof. unfold interp_fail,interp. unfold Basics.iter, failT_iter, Basics.iter, MonadIter_itree. rewrite unfold_iter. cbn. destruct (observe t). cbn; repeat (rewrite ?bind_bind, ?bind_ret_l, ?bind_map; try reflexivity). cbn; repeat (rewrite ?bind_bind, ?bind_ret_l, ?bind_map; try reflexivity). cbn; repeat (rewrite ?bind_bind, ?bind_ret_l, ?bind_map; try reflexivity). apply eq_itree_clo_bind with (UU := Logic.eq); [reflexivity | intros x ? <-]. destruct x as [x|]. - rewrite bind_ret_l; reflexivity. - rewrite bind_ret_l; reflexivity. Qed.
imports: Coq(Morphisms) Paco(paco) ITree(Basics.Utils Basics.Basics Basics.Category Basics.CategoryKleisli Basics.HeterogeneousRelations Basics.Monad Core.ITreeDefinition Core.KTree Core.KTreeFacts Eq.Eqit Eq.UpToTaus Eq.Paco2 Indexed.Sum Interp.Interp Interp.InterpFacts Interp.RecursionFacts)