proposition: Lemma finite_codomain : forall As (f : nat -> A), (forall i, In (f i) As) -> exists a, exists g, (forall i, g i < g (S i)) /\ (forall i, f (g i) = a) /\ (forall i, f i = a -> exists j, i = g j).
proof: Proof. induction As; intros f fin. ded (fin 0). intuition. destruct (classic (forall i, exists j, j >= i /\ f j = a)). exists a. exists (g H). intuition. apply g_mon. apply g_correct. apply g_complete. hyp. rewrite not_forall_eq in H. destruct H as [i0 hi0]. rewrite not_exists_eq in hi0. set (f' := fun i => f(i0+i)). assert (forall i, In (f' i) As). intro i. ded (fin (i0+i)). simpl in H. destruct H. 2: hyp. ded (hi0 (i0+i)). rewrite not_and_eq in H0. destruct H0. absurd (i0+i>=i0). hyp. lia. subst. cong. destruct (IHAs f' H) as [b [g [h1 [h2 h3]]]]. exists b. exists (prefix f b i0 g). intuition. apply prefix_mon. hyp. apply prefix_correct. hyp. apply prefix_complete. intros j hj e. unfold f' in h3. assert (j = i0 + (j-i0)). lia. rewrite H1 in e. destruct (h3 _ e) as [k hk]. exists k. lia. hyp. Qed.
imports: CoLoR(RelUtil NatUtil Path LeastNat LogicUtil ClassicUtil SN NotSN_IS SortUtil ListUtil) Coq(IndefiniteDescription)