proposition: Lemma SmNotPR : isPR 1 (fun n => S (m n)) -> False.
proof: Proof. intro; eapply dom_AckNotPR; eauto. apply m_dominates_Ack; auto. Qed.
imports: hydras(Hydra_Lemmas Epsilon0_Needed_Free Epsilon0_Needed_Std Hydra_Termination L_alpha Battle_length Ack) hydras(primRec F_alpha AckNotPR PrimRecExamples F_omega)