An exact proof term for the current goal is binintersectE1.