proposition: Lemma freePtUn A h x (v : A) : def (x :-> v :+ h) -> free x (x :-> v :+ h) = h.
proof: Proof. move=>D; rewrite freeUnr; last by rewrite (defPt_dom D). by rewrite freeU eqxx (negbTE (defPt_null D)) free0 un0h. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep