Unique solutions of contractions, CCS, and their HOL formalisation