added inter_eq, difference and toAList to sptreeTheory
minor updates to Milawa proofs