The Contrapositive command can only be used when you have a goal of the form P→Q. If you select a goal of this form and give the Contrapositive command, then Proof Designer will create a subproof in which it is assumed that Q is false, and it will say that to complete the subproof you must prove ¬P.