proposition: Lemma phi_to_L n : forall phi, forall p, dp_eval phi (fun _ => 0) p = eval (@conv n p) (L_from phi).
proof: Proof. induction p; cbn. - reflexivity. - now rewrite L_nth. - invert pos p. - destruct d; cbn; congruence. 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