This directory contains: grundlagen_0.aut: original specification valid in AutQE with η-reduction enabled grundlagen_1.aut: "η-equivalent" specification valid also in λδ version 3 grundlagen_2.aut: "η-equivalent" specification valid also in a Pure Type System