proposition: Lemma poly_eqb_spec p1 p2 : reflect (p1 = p2) (poly_eqb p1 p2).
proof: Proof. revert p2; induction p1; destruct p2; cbn. all: try destruct d; try destruct d0; try now (econstructor; congruence). - destruct (Nat.eqb_spec n n0); subst; econstructor; congruence. - destruct (Nat.eqb_spec n n0); subst; econstructor; congruence. - destruct (IHp1_1 p2_1), (IHp1_2 p2_2); cbn; econstructor; congruence. - destruct (IHp1_1 p2_1), (IHp1_2 p2_2); cbn; econstructor; 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