proposition: Lemma pts_injP A1 A2 x1 x2 (v1 : A1) (v2 : A2) : def (x1 :-> v1) -> x1 :-> v1 = x2 :-> v2 -> x1 = x2 /\ A1 = A2.
proof: Proof. rewrite /pts /upd /=. by case: decP=>H1; case: decP=>H2 // _; case. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep