A Labeled Natural Deduction System for a Fragment of CTL∗