proposition: Lemma L_spec_unicity alpha f g : L_spec alpha f -> L_spec alpha g -> forall k, f (S k) = g (S k).
proof: Proof. inversion 1. - subst; inversion 1. + intros; now rewrite H0, H2. + now destruct H2. - inversion 1. + subst; now destruct H0. + intro k; specialize (mlarge_unicity alpha _ _ _ (H1 k) (H6 k)). intro H9; assert (S k < f (S k))%nat by (eapply L_pos_inv; eauto). assert (S k < g (S k))%nat by (eapply L_pos_inv; eauto). abstract lia. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)