fact: Fixpoint select (A: list nat) (B: list X) := match A with | nil => nil | i :: A => match nth B i with | Some x => x :: select A B | None => select A B end end.
imports: List Arith Lia Undecidability.HOU(std.tactics std.lists.basics std.decidable)