proposition: Lemma freeU h x y d : free x (upd h y d) = if x == y then if y == null then Undef else free x h else upd (free x h) y d.
proof: Proof. case: h=>[|h H] /=; first by case: ifP=>// E; case: ifP. rewrite /upd; case: ifP=>E1; case: decP=>H1 //. - by rewrite (negbTE H1); apply/heapE; rewrite rem_ins E1. - by case: ifP H1=>// ->. by apply/heapE; rewrite rem_ins E1. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep