Mechanizing type environments in weak HOAS

We provide a paradigmatic case study, about the formalization of System F<:F<:'s type language in the proof assistant Coq. Our approach relies on weak HOAS, for the sake of producing a readable and concise representation of the object language. Actually, we present and discuss two encoding strategies for typing environments   which yield a remarkable influence on the whole formalization. Then, on the one hand we develop System F<:F<:'s metatheory, on the other hand we address the equivalence of the two approaches internally to Coq.