for A being set holds the_unity_wrt (FinPairUnion A) = [({}. A),({}. A)]