proposition: Lemma subdomPE A B x (v1 : A) (v2 : B) : x != null -> subdom (x :-> v1) (x :-> v2).
proof: Proof. move=>H; rewrite /subdom /pts /upd /=; case: decP=>//= _. rewrite (_ : FinMap _ = ins x (dyn v2) (finmap.nil _ _)) //. by rewrite supp_ins inE /= eq_refl. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep