"subsubsubsublemma" kind of cracked me up. He seems very dedicated to not numbering the nested schema in this proof. :-)