proposition: Lemma iota_iotas : forall alpha, nf alpha -> node (iotas alpha) = iota alpha .
proof: Proof. induction alpha. - reflexivity. - intros; now cbn. Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )