proposition: Theorem ra_eq_dec k (a : recalg k) (b : recalg k) : { a = b } + { a <> b }.
proof: Proof. exact (ra_eq_dec_rec a b eq_refl). Qed.
imports: Arith Lia List Bool Eqdep_dec Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list finite pos vec) Undecidability.MuRec.MuRec