proposition: Lemma cancelT A1 A2 h1 h2 x (v1 : A1) (v2 : A2) : def (x :-> v1 :+ h1) -> x :-> v1 :+ h1 = x :-> v2 :+ h2 -> A1 = A2.
proof: Proof. move=>D E. have: look x (x :-> v1 :+ h1) = look x (x :-> v2 :+ h2) by rewrite E. by rewrite !lookPtUn -?E //; apply: dyn_injT. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep