proposition: Lemma canonS_limit_lub (lambda : T1) : nf lambda -> T1limit lambda -> strict_lub (fun i => canon lambda( S i)) lambda.
proof: Proof. split. - intros; split. + now apply nf_canon. + split; trivial. * apply canon_lt; auto. intro H1;subst; discriminate. - intros l' Hl'; assert (nf l'). { specialize (Hl' 0). eauto with T1. } destruct (T1.lt_eq_lt_dec lambda l'). + repeat split;auto. destruct s. * now left. * subst; now right. + assert (l' t1< lambda)%t1 by (split; auto). destruct (canonS_limit_strong H H0 H2). specialize (Hl' x). assert (l' t1< l')%t1. { apply LT_LE_trans with (canon lambda (S x)); auto. } now destruct (@LT_irrefl l' ). Qed.
imports: hydras.Prelude(DecPreOrder)