proposition: Remark R2 : mlarge (cnf alpha) (interval (S k) (Nat.pred l)).
proof: Proof. unfold l; generalize (L_correct alpha). inversion 1; auto. destruct alpha; auto. - rewrite E0_eq_iff in Halpha; simpl in Halpha, H0; subst cnf; now destruct Halpha. Qed.
imports: hydras(L_alpha) hydras(Hydra_Lemmas Epsilon0_Needed_Free Epsilon0_Needed_Std Hydra_Termination O2H)