Finally proved the irrelevance transformation to be correct with respect to propositional equality.