for A being set holds {}. A is_a_unity_wrt FinUnion A