proposition: Lemma all_finite_translate {E F R}: forall (f: E ~> F) (t: itree E R), all_finite t -> all_finite (translate f t).
proof: Proof. intros *; induction 1; rewrite unfold_translate, H; cbn. - apply all_finite_Ret. - apply all_finite_Tau. auto. - apply all_finite_Vis. auto. Qed.
imports: ITree(ITree Basics.Utils Eq.Eqit Interp.TranslateFacts Leaf) ITree.Events(Nondeterminism Exception) Paco(paco) Coq(Morphisms Basics Program.Equality)