proposition: Lemma iota_succ_round_n : forall i alpha, nf alpha -> round_n i (iota (T1.succ alpha)) (iota alpha).
proof: Proof. left; now apply iota_succ_R1. Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )