proposition: Lemma iota_succ_R1 : forall o, nf o -> R1 (iota (T1.succ o)) (iota o).
proof: Proof. intros; repeat rewrite <- iota_iotas; auto. - rewrite iotas_succ; auto ; constructor. replace (iotas o) with (hy_app (iotas o) hnil) at 2. + apply S0_app ; constructor. + now rewrite hy_app_l_nil. - now apply succ_nf. Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )