proposition: Lemma red : H10 ⪯ (fun '(p1, p2) => exists L, eval p1 L = eval p2 L).
proof: Proof. unshelve eexists. - intros (n & p1 & p2). exact (conv p1, conv p2). - intros (n & p1 & p2). cbn. unfold dio_single_pred. cbn. split. + intros [phi]. exists (L_from phi). now rewrite <- !phi_to_L. + intros [L]. exists (fun n => nth (pos.pos2nat n) L 0). now rewrite !phi_to_L, !eval_L_from. Qed.
imports: Undecidability.H10(H10 dio_single dio_logic) Undecidability.PCP.Util.PCP_facts Undecidability.Shared.Libs.PSL.FiniteTypes Undecidability.L.Datatypes(LNat LProd) Undecidability.L(Tactics.LTactics Computability.MuRec Computability.Synthetic Tactics.GenEncode) Undecidability.Shared.Libs.DLW.Vec(pos) Undecidability.L.Datatypes.List(List_basics List_extra) Nat Datatypes