Add proof of lemma on switching to strict henselizations
Standard material about Galois extensions of ff of dvrs