Support multiset union in the proof mode.

7 jobs for master in 24 minutes and 57 seconds