proposition: Lemma L_omega_ok : L_spec T1omega L_omega.
proof: Proof. pose (H:= L_lim_ok T1omega nf_omega refl_equal L_fin (fun i => L_fin_ok (S i))). eapply L_spec_compat with (1:=H); intro ; unfold L_lim, L_fin, L_omega; abstract lia. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)