A Sequent Calculus for First-Order Dynamic Logic with Trace Modalities