Free theorems, where?
The formulas are formulas of Abadi-Plotkin logic, which they describe in their paper A Logic for Parametric Polymorphism. 

The semantics of System F that Abadi and Plotkin used to interpret their logic can be found in Bainbridge, Freyd, Scedrov, Scott's paper Functorial Polymorphism.