Coq implementation of SF-calculus and the tranlsation to it of lift lambda-calculus - View it on GitHub