proposition: Lemma F_alpha_PR_inv: forall alpha, isPR 1 (F_ alpha) -> alpha o< E0_omega.
proof: Proof. intro alpha. destruct (E0_lt_ge alpha E0_omega); auto. intro H0; destruct ( F_alpha_not_PR _ H H0). Qed.
imports: hydras(Iterates F_alpha E0 Ack AckNotPR) Coq(ArithRing Lia Arith)