proposition: Theorem KS_thm_2_4_E0 : forall lambda, E0limit lambda -> forall i j, (i < j)%nat -> Canon_plus 1 (Canon lambda (S j)) (Canon lambda (S i)).
proof: Proof. intros; destruct lambda; cbn; apply KS_thm_2_4;auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)