proposition: Lemma cancel A h1 h2 x (v1 v2 : A) : def (x :-> v1 :+ h1) -> x :-> v1 :+ h1 = x :-> v2 :+ h2 -> [/\ v1 = v2, def h1 & h1 = h2].
proof: Proof. move=>D E. have: look x (x :-> v1 :+ h1) = look x (x :-> v2 :+ h2) by rewrite E. rewrite !lookPtUn -?E // => /dyn_inj X. by rewrite -{}X in E *; rewrite -(unhKl D E) (defUnr D). Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep