proposition: Lemma list_choice {P : nat -> nat -> Prop} {l: list nat} : Forall (fun i : nat => exists n : nat, P i n) l -> exists φ, Forall (fun i : nat => P i (φ i)) l.
proof: Proof. elim: l; first by exists id. move=> k l IH /Forall_cons_iff [[n Hkn]] /IH [φ Hφ]. exists (fun i => if PeanoNat.Nat.eq_dec i k then n else φ i). constructor; first by case: (PeanoNat.Nat.eq_dec k k). apply: Forall_impl Hφ => i Hi. case: (PeanoNat.Nat.eq_dec i k); [by move=> /= ->|done]. Qed.
imports: List Lia ssreflect ssrbool ssrfun