proposition: Lemma MPCPsimp_MPCP c C: MPCPsimp (c,C) <-> MPCP (c,C).
proof: Proof. split. + intros [C' H]. rewrite incl_select_iff in H. destruct H as ((I & ? & ?) & ?); subst. exists I. rewrite <-!select_map; intuition. + intros (I & H). exists (select I (c :: C)). rewrite incl_select_iff. intuition eauto. rewrite !select_map; intuition. Qed.
imports: List Undecidability.HOU(std.std)