proposition: Lemma canonS_iota i a : nf a -> a <> 0 -> iota a -1-> iota (canon a (S i)).
proof: Proof. intros; destruct (canonS_iota_i i a H H0). - exists 0; now left. - exists i; now right. Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )