proposition: Corollary Alive_free : Alive free.
proof: Proof. red;intros. destruct (next_round i h). - destruct s as [h' H']; exists h'; now exists i. - tauto. Qed.
imports: hydras(Hydra_Lemmas Epsilon0_Needed_Free Epsilon0_Needed_Std Hydra_Termination L_alpha Battle_length Ack)