proposition: Fact DFt : any_finite t.
proof: Proof. apply any_finite_Vis with true; auto with itree. Qed.
imports: ITree(ITree Basics.Utils Eq.Eqit Interp.TranslateFacts Leaf) ITree.Events(Nondeterminism Exception) Paco(paco) Coq(Morphisms Basics Program.Equality)