proposition: Theorem Variant_LT_standard : @Hvariant _ _ T1_wf standard Hydra_Termination.m.
proof: Proof. split; intros i h h' H H0; apply round_decr; now exists i. Qed.
imports: hydras(Hydra_Lemmas Epsilon0_Needed_Free Epsilon0_Needed_Std Hydra_Termination L_alpha Battle_length Ack)