added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
(*<*)theory Paperimports "../Quot/QuotMain"begin(*>*)section {* Introduction *}text {* Here can come any text.*}(*<*)end(*>*)