proposition: Lemma iotas_succ : forall alpha, nf alpha -> iotas (T1.succ alpha) = hy_app (iotas alpha) (hcons head hnil).
proof: Proof. induction alpha. - cbn; trivial. - destruct alpha1; intros. + T1_inversion H. subst alpha2; replace (cons zero n zero) with (FS n). * rewrite succ_compatS; cbn; clear H; induction n;simpl;auto. repeat f_equal; injection IHn; auto. * reflexivity. + rewrite succ_rw1; simpl hy_app. simpl iotas; repeat f_equal; rewrite <- hcons_mult_app; rewrite IHalpha2; auto. * eauto with T1. * discriminate. Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )