Text this: A formal proof of the factor price equalization theorem