Modeling a CPS translation from STLC to System F in Coq using Locally Nameless