proposition: Lemma pts_inj A x (v1 v2 : A) : def (x :-> v1) -> x :-> v1 = x :-> v2 -> v1 = v2.
proof: Proof. move=>D; rewrite /pts /upd. case: decP; last by rewrite -(defPt _ v1) D. by move=>H []; apply: inj_pairT2. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep