We give a machine-checked proof of the equivalence of the usual, two-sorted presentation of System F and its single-sorted pure type system variant λ2. This is established by reducing the typability problem of F to λ2 and vice versa. The systems are formulated using higher-order abstract syntax and the proof is executed in the Abella proof system. We compare and contrast this proof to our earlier Coq formalisation based on de Bruijn indices and context morphism lemmas.
Further details, including Abella sources on project page.