This merge request adds a proposed proof for the associativity of substitution, along with some cleanup.