preamble.etc: nicer implies, comments on abbr.
AIntroductoryProblems.1.a: CTL properties