proposition: Lemma large_omega_2 : forall s n, ~In 0 (n::s) -> (n <= List.length s)%nat -> gnaw T1omega (n::s) = zero.
proof: Proof. intros; cbn; destruct n. destruct H; now left. apply gnaw_n_R; auto. intro; destruct H; now right. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)