proposition: Lemma freeF h x y : free x (free y h) = if x == y then free x h else free y (free x h).
proof: Proof. by case: h=>*; case: ifP=>E //; apply/heapE; rewrite rem_rem E. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep