proposition: Lemma canon_lim2 i n lambda : nf lambda -> T1limit lambda -> canon (cons lambda (S n) zero) i = cons lambda n (T1.phi0 (canon lambda i)).
proof: Proof. destruct i; intros. - now apply canon0_lim2. - now apply canonS_lim2. Qed.
imports: hydras.Prelude(DecPreOrder)