Serious progress towards TypingWellFormednessProof, 4 qed with 11 admits.