fact: Definition union2 h1 h2 := nosimpl (if (h1, h2) is (Def hs1 ns1, Def hs2 ns2) then if disj hs1 hs2 then Def (@un_nullP _ _ ns1 ns2) else Undef else Undef).
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep