proposition: Lemma L06: rounds standard k (iota (cnf alpha)) (l-1)%nat (iota zero).
proof: Proof. rewrite <- R6; apply trace_to_std. generalize R0; abstract lia. apply R5. Qed.
imports: hydras(L_alpha) hydras(Hydra_Lemmas Epsilon0_Needed_Free Epsilon0_Needed_Std Hydra_Termination O2H)