proposition: Lemma starp0 p : p # emp <~> p.
proof: Proof. move=>h /=; split; first by case=>h1 [h2][->][H1]->; rewrite unh0. by move=>H1; exists h; exists empty; rewrite unh0. Qed.
imports: mathcomp(ssreflect ssrfun) LemmaOverloading(rels heaps)