fact: Fixpoint modify (u: table (option term)) (a:term) {struct a} : term := match a with X i => let g := get (nat_pos i) u in match g with none => X i | some t => t end | const s => const s | ev x y => ev (modify u x) (modify u y) end.