Tweak extensionality proof.