proposition: Lemma dom_look h x : x \notin dom h -> look x h = dyn tt.
proof: Proof. by case: h=>[|h H] //; rewrite /look /dom -topredE /=; case: (suppP x)=>// ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep