proposition: Lemma l_std_ok : forall alpha : E0, alpha <> E0zero -> forall k : nat, 1 <= k -> battle_length standard k (iota (cnf alpha)) (l_std alpha k).
proof: Proof. apply battle_length_std. Qed.
imports: hydras(L_alpha) hydras(Hydra_Lemmas Epsilon0_Needed_Free Epsilon0_Needed_Std Hydra_Termination O2H)