proposition: Lemma L_omega_mult_ok (i: nat) : L_spec (T1omega * i) (L_omega_mult i).
proof: Proof. destruct i. - left; intro k; reflexivity. - right. + cbn; discriminate. + intros k; unfold L_omega_mult, L_omega; apply omega_mult_mlarge_0. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)