proposition: Lemma o2iota_1 : forall j beta i alpha, standard_path_to j beta (S i) alpha -> nf alpha -> nf beta -> beta <> T1.zero -> rounds standard i (iota alpha) j (iota beta) .
proof: Proof. intros; change i with (Nat.pred (S i)); apply o2iota_0; trivial. auto with arith. Qed.
imports: hydras(Epsilon0_Needed_Generic)