proposition: Lemma domU h y d : dom (upd h y d) =i [pred x | (y != null) && if x == y then def h else x \in dom h].
proof: Proof. case: h=>[|h T] /= x; rewrite inE /upd /=. - rewrite ?inE. case: ifP=>//; rewrite andbF; reflexivity. case: ifP=>E; case: decP=>H1; rewrite /dom /=. - by rewrite (eqP E) H1 supp_ins inE /= eq_refl. - by case: eqP H1. - by rewrite supp_ins inE /= E H1. by case: eqP H1. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep