proposition: Lemma Lemma_4_4_2 : forall (s : list nat) (n : nat) (alpha beta : T1), nf alpha -> nf beta -> sorted_ge n s -> const_pathS_eps n alpha beta -> gnawS beta s t1<= gnawS alpha s.
proof: Proof. intros; specialize (@Lemma_4_4_1 s n alpha beta H H0 H1 H2). intro H4; eapply const_pathS_eps_LE_2; eauto. all: eapply gnawS_nf; eauto. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)