proposition: Lemma defUn : forall h1 h2, defUn_spec h1 h2 (def (h1 :+ h2)).
proof: Proof. case=>[|h1 H1][|h2 H2] /=; try by [apply: def_false1 | apply: def_false2]. rewrite /union2; case: ifP=>E. - by apply: def_true=>// x H; case: disjP E=>//; move/( _ _ H). by case: disjP E=>// x T1 T2 _; apply: (def_false3 (x:=x)). Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep