proposition: Lemma hfresh_null h : hfresh h != null.
proof: Proof. by case: h=>[//|[h H] F]; rewrite /lfresh ptrE -lt0n /= addnS. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep