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