proposition: Lemma canonS_limit_mono alpha i j : nf alpha -> T1limit alpha -> i < j -> canon alpha (S i) t1< canon alpha (S j).
proof: Proof. intros; eapply canon_limit_mono; eauto. auto with arith. Qed.
imports: hydras.Prelude(DecPreOrder)