Library Imp_LangTrick.Examples.ProofCompExamples