proposition: Lemma lookF h x y : look x (free y h) = if x == y then dyn tt else look x h.
proof: Proof. by case: h=>[|h H]; case: ifP=>E //; rewrite /look /free fnd_rem E. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep