Add stubs for some more eta facts
Add proof of eta-postponement!
Add proofs about eta's
Add proof that eta_par is substitutive

Final `admit` (except for the lift / subst lemmas) eliminated!