This is an old development which could be improved in many ways
We formalize the λj-calcus and prove that it enjoys Full Composition. Tested with Coq 8.3pl1.