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