proposition: Lemma subheapUn h1 h2 h1' h2' : def (h2 :+ h2') -> subheap h1 h2 -> subheap h1' h2' -> subheap (h1 :+ h1') (h2 :+ h2').
proof: Proof. move=>defs [Sd1 Sl1] [Sd2 Sl2]. split=>[|x]; first by apply: subdomUE. rewrite domUn inE /= inE /=; case/andP=>D; case/orP=>H. - by rewrite !lookUnl // H Sl1 // (subdomQ Sd1 H). by rewrite !lookUnr // H Sl2 // (subdomQ Sd2 H). Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep