Proof of squash_thru_equiv_rel