proposition: Lemma select_repeated n I x: I ⊆ nats n -> select I (repeat x n) = repeat x (length I).
proof: Proof. induction I; cbn; eauto; intros. rewrite IHI; eauto with listdb. edestruct (nth_error_lt_Some) as [y H']; try rewrite H'. eapply nats_lt; lsimpl; firstorder. now eapply nth_error_In, repeated_in in H'; subst. Qed.
imports: List Arith Lia Undecidability.HOU(std.tactics std.lists.basics std.decidable)