A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value λ-Calculus Academic Article