proposition: Lemma select_S I (x: X) A: select (map S I) (x :: A) = select I A.
proof: Proof. induction I. - reflexivity. - cbn. rewrite IHI. reflexivity. Qed.
imports: List Arith Lia Undecidability.HOU(std.tactics std.lists.basics std.decidable)