proposition: Lemma canon_lim1 : forall i lambda, nf lambda -> T1limit lambda -> canon (cons lambda 0 zero) i = T1.phi0 (canon lambda i).
proof: Proof. destruct i. - 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. - intros; apply canonS_lim1; auto. Qed.
imports: hydras.Prelude(DecPreOrder)