proposition: Lemma injUh A h1 h2 x (v1 v2 : A) : def (h1 :+ (x :-> v1)) -> h1 :+ (x :-> v1) = h2 :+ (x :-> v2) -> def h1 /\ h1 = h2 /\ v1 = v2.
proof: Proof. by rewrite -!(unC (x :-> _))=>D; case/(cancel D)=><- -> ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep