proposition: Lemma L_omega_cube_ok : L_spec (T1.phi0 3) L_omega_cube.
proof: Proof. unfold L_omega_cube; apply L_lim_ok; auto with T1. - intro k; simpl canon; apply L_omega_square_times_ok. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)