proposition: Theorem LNotPR : False.
proof: Proof. apply SmNotPR, compose1_1IsPR. - apply mIsPR. - apply succIsPR. 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)