proposition: Lemma subdomUE h1 h2 h1' h2' : def (h2 :+ h2') -> subdom h1 h2 -> subdom h1' h2' -> subdom (h1 :+ h1') (h2 :+ h2').
proof: Proof. case: h1 h2 h1' h2'=>[|h1 H1] [|h2 H2] [|h1' H1'] [|h2' H2'] //. rewrite /subdom /def /union2. case: ifP=>E1 // _; case: ifP=>E2 // T1 T2; last first. - case: disjP E2=>// x; case: allP T1=>// X _; move/X=>{X}. case: disjP E1=>// X _; move/X=>{X}. by case: allP T2=>// X _ H3 H4; move/X: H4 H3=>->. case: allP=>//; case=>x. rewrite !supp_fcat !inE; case/orP=>E. - by case: allP T1=>//; move/(_ _ E)=>->. by case: allP T2=>//; move/(_ _ E)=>->; rewrite orbT. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep