proposition: Lemma loweqE h1 h2 : h1 =~ h2 -> lfresh h1 = lfresh h2.
proof: Proof. by rewrite /loweq /lfresh; move/eqP=>->. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep