proposition: Lemma cancel2 : forall h1 h2 : heap, h1 = h2 -> h1 :+ empty = h2.
proof: Proof. by move=>h1 h2 ->; apply: unh0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool ssrnat seq eqtype) LemmaOverloading(prelude prefix heaps terms)