added section for extensionality/relevance with explain section — formal statement and proof to come still. also some typo corrections in the structures file