proposition: Lemma incl_select_iff X (A B: list X): A ⊆ B <-> exists I, I ⊆ nats (length B) /\ select I B = A.
proof: Proof. split. - now intros ? % incl_select. - intros [I [? <-]]; eapply select_incl. Qed.
imports: List Undecidability.HOU(std.std)