proposition: Lemma incl_select A B: A ⊆ B -> exists I, I ⊆ nats (length B) /\ select I B = A.
proof: Proof. induction A. + exists nil. lauto. + intros; destruct IHA as [I []]; lauto. specialize (H a). mp H; lauto. eapply In_nth_error in H as [i]. exists (i::I). cbn. rewrite H, H1. split; lauto. eapply nth_error_Some_lt, lt_nats in H; lauto. Qed.
imports: List Arith Lia Undecidability.HOU(std.tactics std.lists.basics std.decidable)