Move lam_k_alt lemma to Eta module, explain it