proposition: Theorem not_all_infinite_any_finite {E A} (t : itree E A) : all_infinite t -> any_finite t -> False.
proof: Proof. intros H1 H2. induction H2; punfold H1; inversion H1; try congruence. all: pclearbot; rewrite H in H0; inversion H0; subst; auto. ddestruction. exact (IHany_finite (H3 _)). Qed.
imports: ITree(Axioms ITree Props.Finite Props.Infinite) Paco(paco)