fact: Definition union_map_classTPCMMix K C V (U : union_map_class C V) := TPCMMixin (@empbP K C V U) (@valid_undefN K C V U) (@undef_join _ _ _ U).
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)