proposition: Lemma heap_ind' (P : heap -> Prop) : P undef -> P Unit -> (forall A x (v : A) f, P f -> valid (x :-> v \+ f) -> P (x :-> v \+ f)) -> forall f, P f.
proof: Proof. move=>H1 H2 H3; apply: um_ind' H1 H2 _. by move=>/= k [A v] f; apply: H3. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)