proposition: Lemma updPtUn A1 A2 x i (v1 : A1) (v2 : A2) : upd (x :-> v1 :+ i) x (dyn v2) = x :-> v2 :+ i.
proof: Proof. case E1: (def (x :-> v1 :+ i)). - by rewrite updUnl domPt inE /= eqxx (defPt_null E1) /= updU eqxx. have E2: def (x :-> v2 :+ i) = false by rewrite !defPtUn in E1 *. by case: (_ :+ _) E1=>// _; case: (_ :+ _) E2. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep