proposition: Lemma canonS_lim1 : forall i lambda, nf lambda -> T1limit lambda -> canon (cons lambda 0 zero) (S i) = T1.phi0 (canon lambda (S i)).
proof: Proof. intros; unfold canon at 1; destruct lambda. - discriminate. - replace ( T1.pred (cons lambda1 n lambda2)) with (@None T1). + f_equal. + rewrite pred_of_limit;auto. Qed.
imports: hydras.Prelude(DecPreOrder)