Automating the synthesis of decision procedures in a constructive metatheory