proposition: Lemma updU h x y d1 d2 : upd (upd h x d1) y d2 = if x == y then upd h x d2 else upd (upd h y d2) x d1.
proof: Proof. case: h =>[|h T]; rewrite /upd; case: ifP=>// H; case: decP=>H1 //; case: decP=>// H2; last 2 first. - by rewrite -(eqP H) H1 in H2. - by apply/heapE; rewrite ins_ins eq_sym H. by apply/heapE; rewrite ins_ins (eqP H) eq_refl. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep