Add partial defs and lemmas from Kashima paper

I seem to have broken something in one of my proofs while merging. Need to look into this with fresh brain.