proposition: Lemma limit_no_R1 : forall alpha, nf alpha -> T1limit alpha = true -> forall h', ~ R1 (iota alpha) h'.
proof: Proof. intros alpha H H0 h' H1; generalize ( limit_no_head _ H H0). intro H2; case_eq (iota alpha); case_eq h';intros. subst h';rewrite <- iota_iotas in H1; auto. generalize (R1_mem_head _ _ H1). tauto. Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )