proposition: Fact fin_reif n : (forall i, i < n -> exists x, R i x) -> exists s, forall i (Hi : i < n), R i (s i Hi).
proof: Proof. assert (H_lt_S_n : forall n m, S n < S m -> n < m) by (now intros; apply Nat.succ_lt_mono). revert R; induction n as [ | n IHn ]; intros R HR. + assert (s : forall x, x < 0 -> X) by (intros; lia). exists s; intros; lia. + destruct (HR 0) as (x & Hx); try lia. destruct IHn with (R := fun i x => R (S i) x) as (s & Hs). { intros; apply HR; lia. } exists (fun i => match i with 0 => fun _ => x | S i => fun Hi => s i (H_lt_S_n i n Hi) end). intros [ | i ] Hi; simpl; auto. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)