proposition: Lemma lookU h x y d : look x (upd h y d) = if x == y then if def h && (y != null) then d else dyn tt else if y != null then look x h else dyn tt.
proof: Proof. case: h=>[|h H] /=; case: ifP=>E //; case: ifP=>H1 //; rewrite /upd; by case: decP=>// H2; rewrite /look fnd_ins E //; rewrite H1 in H2. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep