Am I missing something, or is the arrow operator (mathematical implication) not quite right in the example code they give? What happens when a statement is vacuously true?