proposition: Lemma ldomK h1 h2 t1 t2 : def (h1 :+ t1) -> def (h2 :+ t2) -> ldom h1 =i ldom h2 -> ldom (h1 :+ t1) =i ldom (h2 :+ t2) -> ldom t1 =i ldom t2.
proof: Proof. move=>D1 D2 H1 H2 x; move: {H1 H2} (H1 x) (H2 x). rewrite !ldomP !domUn !inE. case: defUn D1=>// H1 H2 L1 _; case: defUn D2=>// H3 H4 L2 _. case E1: (x \in dom t1); case E2: (x \in dom t2)=>//; rewrite orbF orbT /=; case E3: (x \in dom h1); case E4: (x \in dom h2)=>//= _ _; by [move/L1: E3; rewrite E1 | move/L2: E4; rewrite E2]. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep