proposition: Remark R4 : trace_to (O2H.iota zero) (unshift (interval (S k) (Nat.pred l))) (O2H.iota (cnf alpha)).
proof: Proof. apply O2H.path_toS_trace; [apply R3 | auto with E0]. Qed.
imports: hydras(L_alpha) hydras(Hydra_Lemmas Epsilon0_Needed_Free Epsilon0_Needed_Std Hydra_Termination O2H)