proposition: Fact fin_reif_nat (R : nat -> nat -> Prop) n : (forall i, i < n -> ex (R i)) -> exists s, forall i, i < n -> R i (s i).
proof: Proof. intros HR. apply fin_reif in HR. destruct HR as (s & Hs). exists (fun i => match le_lt_dec n i with left _ => 0 | right H => s _ H end). intros i Hi; destruct (le_lt_dec n i); auto; lia. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)