proposition: Lemma L_omega_square_times_ok i : L_spec (T1.cons 2 i zero) (L_omega_square_times (S i)).
proof: Proof. apply L_phi0_mult_ok. - auto with T1. - apply L_omega_square_Sle. - apply L_omega_square_ok. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)