Added reasons to statements in proofs; added union rule; corrected set
equality proof