fact: Fixpoint L_poly n : list (poly) := match n with | 0 => [] | S n => L_poly n ++ map poly_cnst (L_nat n) ++ map poly_var (L_nat n) ++ map poly_add' (list_prod (L_poly n) (L_poly n)) ++ map poly_mul' (list_prod (L_poly n) (L_poly n)) end.
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