proposition: Lemma canonS_lim2 i n lambda: nf lambda -> T1limit lambda -> canon (cons lambda (S n) zero) (S i) = cons lambda n (T1.phi0 (canon lambda (S i))).
proof: Proof. intros; cbn; destruct lambda. - simpl; discriminate. - remember (cons lambda1 n0 lambda2) as lambda. replace (pred lambda) with (@None T1). + trivial. + now rewrite pred_of_limit. Qed.
imports: hydras.Prelude(DecPreOrder)