proposition: Lemma congUh A h1 h2 x (v1 v2 : A) : h1 = h2 -> v1 = v2 -> h1 :+ (x :-> v1) = h2 :+ (x :-> v2).
proof: Proof. by move=>-> ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep