proposition: Lemma heap_eta h x : x \in dom h -> h = upd (free x h) x (look x h).
proof: Proof. case: h=>[|h H] //; rewrite /upd /look /dom /free. case: decP; rewrite -topredE => /= H1 H2; last first. - by case: eqP H1 H H2=>// -> _ H; rewrite (negbTE H). apply/heapE; apply: fmapP=>k; rewrite fnd_ins. case: ifP=>[|E]; last by rewrite fnd_rem E. move/eqP=>->; case E1: (fnd x h)=>//. by case: (suppP _ h) H2 E1=>// v ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep