simp [advance]
tag : Tag
time : Time.From tag.time
⊢ (advance tag time).time = time.val
tag : Tag
time : Time.From tag.time
⊢ (if tag.time < time.val then { time := time.val, microstep := 0 } else increment tag).time = time.val