proposition: Lemma canonS_iota_final : round_n i (iota alpha) (iota (canon alpha (S i))).
proof: Proof. destruct all_cases as [beta [n [gamma Heq]]]; decompose [and] Heq. destruct (zero_limit_succ_dec Halpha). - destruct s. + contradiction. + destruct n. * destruct (zero_limit_succ_dec H). { destruct s. - subst beta; rewrite H2 in Halpha. generalize (nf_of_finite Halpha). intro; subst gamma alpha. simpl iota; left. split; left. - destruct gamma. + eapply DS_iota_2 with beta; auto. + eapply canonS_iota_6. eexact H1. discriminate. eexact H2. } destruct gamma. { destruct s as [gamma' [H3 H4]]. subst beta; eapply DS_iota_3 ; eauto. } eapply canonS_iota_6. eexact H1. discriminate. eauto. * destruct gamma. { destruct(zero_limit_succ_dec H). - destruct s. + subst beta alpha; left. split. simpl (hcons_mult head (S (S n)) hnil). left. + eapply canonS_iota_4. eexact H. auto. eauto. - destruct s as [gamma [H3 H4]]. subst beta; eapply canonS_iota_5. eexact H3. eauto. } eapply canonS_iota_6. eexact H1. discriminate. eauto. - destruct s as [delta [H3 H4]]. eapply DS_iota_1; eauto. Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )