proposition: Lemma PCPsimp_PCP C: PCPsimp C <-> PCP C.
proof: Proof. split. + intros [C' H]. rewrite incl_select_iff in H. destruct H as ((I & ? & ?) & ? & ?); subst. exists I. rewrite <-!select_map; intuition. subst; cbn in *; intuition. + intros (I & H). exists (select I C). rewrite incl_select_iff. intuition eauto. destruct I; intuition. cbn in H1. specialize (H0 n); mp H0; lauto. eapply nats_lt, nth_error_lt_Some in H0 as [? ?]. rewrite H0 in H1; discriminate. rewrite !select_map; intuition. Qed.
imports: List Undecidability.HOU(std.std)