proposition: Lemma select_incl I A: select I A ⊆ A.
proof: Proof. induction I; cbn; intuition (try easy). destruct nth eqn: H1; intuition idtac. eapply nth_error_In in H1. intuition (auto with datatypes). Qed.
imports: List Arith Lia Undecidability.HOU(std.tactics std.lists.basics std.decidable)