proposition: Lemma canon0_lim2 n lambda: nf lambda -> T1limit lambda -> canon (cons lambda (S n) zero) 0 = cons lambda n (T1.phi0 (canon lambda 0)).
proof: Proof. intros; cbn; destruct lambda. - simpl; discriminate. - replace ( T1.pred (cons lambda1 n0 lambda2)) with (@None T1); f_equal. rewrite T1.pred_of_limit;auto. Qed.
imports: hydras.Prelude(DecPreOrder)