proposition: Lemma enum_ext (E: enumerates f s) : exists f, enumerates f s /\ forall i j (Li : lt_size i s) (Lj: lt_size j s) (R: r (f i) (f j)), i < j.
proof: Proof. exists (fun n => nth n (prefix_of_nat n) (f 0)); split. { red in E; des; [left|right]; splits; try exists n; splits. { ins; destruct (nth_in_or_default i (prefix_of_nat i) (f 0)) as [X|X]; [apply in_prefix_of_nat_in in X| rewrite X]; eauto. } { ins. revert EQ. apply wlog_lt with (x := i) (y := j); ins; [|by symmetry; eauto]. assert (L: y < length (prefix_of_nat y)). { apply length_prefix_of_nat; eauto. red; intros; eapply INJ in H1; desf; lia. } assert (Lx: x < length (prefix_of_nat x)). { apply length_prefix_of_nat; eauto. red; intros; eapply INJ in H1; desf; lia. } forward apply prefix_of_nat_prefix with (i := x) (j := y) as X; desc; try lia. forward apply nodup_prefix_of_nat with (n:=y) as Y; try done. rewrite NoDup_nth with (d := f 0) in Y; apply Y; eauto; try lia. rewrite X at 1; rewrite nth_app; desf; lia. } { ins; apply SUR in IN; desf. forward apply in_prefix_of_nat with (i := i) (j := i) as X; ins. apply in_split in X; desf. exists (length l1). destruct (le_lt_dec i (length l1)) as [Y|Y]. apply prefix_of_nat_prefix in Y; desc. rewrite Y, X, appA, nth_app; desf; try lia. rewrite Nat.sub_diag; done. forward apply (@prefix_of_nat_prefix (length l1) i) as Z; desc; try lia. forward apply length_prefix_of_nat with (n := length l1); eauto. red; intros; apply INJ in H0; desf; lia. rewrite Z in X; symmetry in X; ins. apply list_app_eq_simpl2 in X; desc; try lia. rewrite X, nth_app, Nat.sub_diag; ins; desf; lia. } { ins; destruct (nth_in_or_default i (prefix_of_nat i) (f 0)) as [X|X]; [apply in_prefix_of_nat_in in X| rewrite X]; eauto. apply RNG; lia. } { ins. revert LTi LTj EQ. apply wlog_lt with (x := i) (y := j); ins; [|by symmetry; eauto]. assert (L: y < length (prefix_of_nat y)). { apply length_prefix_of_nat; [|intros; apply RNG; lia]. red; intros; eapply INJ in H1; desf; lia. } assert (Lx: x < length (prefix_of_nat x)). { apply length_prefix_of_nat; [|intros; apply RNG; lia]. red; intros; eapply INJ in H1; desf; lia. } forward apply prefix_of_nat_prefix with (i := x) (j := y) as X; desc; try lia. forward apply nodup_prefix_of_nat with (n:=y) as Y; try done. rewrite NoDup_nth with (d := f 0) in Y; apply Y; eauto; try lia. rewrite X at 1; rewrite nth_app; desf; lia. } { ins; apply SUR in IN; desf. forward apply in_prefix_of_nat with (i := i) (j := i) as X; ins; eauto. apply in_split in X; desf. exists (length l1). destruct (le_lt_dec i (length l1)) as [Y|Y]. apply prefix_of_nat_prefix in Y; desc. rewrite Y, X, appA, nth_app; desf; try lia. rewrite Nat.sub_diag; splits; ins. assert (length (prefix_of_nat i) <= n). { generalize (nodup_prefix_of_nat i), (fun x => in_prefix_of_nat_in x i). generalize (prefix_of_nat i); clear -SUR; ins. assert (X: forall x, In x l -> In x (map f (List.seq 0 n))). by intros; apply H0, SUR in H1; desf; apply in_map, in_seq0_iff. clear SUR H0. eapply NoDup_incl_length in X; ins. by rewrite length_map, length_seq in *. } rewrite X, length_app in *; ins; lia. forward apply (@prefix_of_nat_prefix (length l1) i) as Z; desc; try lia. forward apply length_prefix_of_nat with (n := length l1). red; intros; apply INJ in H0; desf; lia. intros; apply RNG; lia. rewrite Z in X; symmetry in X; ins. apply list_app_eq_simpl2 in X; desc; try lia. rewrite X, nth_app, Nat.sub_diag; splits; ins; desf; lia. } } intros. destruct (lt_eq_lt_dec j i) as [[]|]; ins; desf; exfalso; [|eby eapply PO]. forward eapply prefix_of_nat_prefix with (i:=j) (j:=i) as X; try lia; desc. red in E; desf. forward eapply length_prefix_of_nat with (n := i) as LEN; try red; ins; desc; eauto. eapply INJ in H0; desf; lia. forward eapply length_prefix_of_nat with (n := j) as LENj; try red; ins; desc; eauto. eapply INJ in H0; desf; lia. forward apply list_before_nth with (l := prefix_of_nat i) (i := j) (j := i) (d := f 0); splits; ins; eauto using nodup_prefix_of_nat. rewrite X in H at 2; rewrite app_nth1 in H; eauto using prefix_nat_r. assert (Lin : i < n). { clear - SUR Li. red in Li; desc. eapply lt_le_trans; eauto. replace n with (length (map f (List.seq 0 n))) by now (rewrite length_map, length_seq). apply NoDup_incl_length; try red; ins. by apply Li0, SUR in H; desf; apply in_map, in_seq0_iff. } forward eapply length_prefix_of_nat with (n := i) as LEN; try red; ins; desc; eauto. eapply INJ in H0; desf; lia. eapply RNG; lia. forward eapply length_prefix_of_nat with (n := j) as LENj; try red; ins; desc; eauto. eapply INJ in H0; desf; lia. eapply RNG; lia. forward apply list_before_nth with (l := prefix_of_nat i) (i := j) (j := i) (d := f 0); splits; ins; eauto using nodup_prefix_of_nat. rewrite X in H at 2; rewrite app_nth1 in H; eauto using prefix_nat_r. Qed.
imports: Arith micromega.Lia Setoid IndefiniteDescription ClassicalChoice HahnBase HahnList HahnEquational HahnRewrite HahnRelationsBasic HahnSets HahnNatExtra HahnListBefore HahnWf HahnSorted HahnTotalExt