proposition: Theorem Variant_lt_free: @Hvariant _ _ E0lt_wf free Hydra_Termination.var.
proof: Proof. split; intros; now apply round_decr. Qed.
imports: hydras(Hydra_Lemmas Epsilon0_Needed_Free Epsilon0_Needed_Std Hydra_Termination L_alpha Battle_length Ack)