proposition: Lemma supdomUh A B h1 h2 x (v1 : A) (v2 : B) : def (h2 :+ (x :-> v2)) -> (def h2 -> supdom h2 h1) -> supdom (h2 :+ (x :-> v2)) (h1 :+ (x :-> v1)).
proof: Proof. move=>H1 H2. apply: subdomUE=>//; first by apply: H2; apply: defUnl H1. by apply: subdomPE; apply: (@defPt_null _ h2 x v2); rewrite unC. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep