split
tag : Tag
t : Time.From tag.time
⊢ tag < if tag.time < t.val then { time := t.val, microstep := 0 } else increment tag
case inl
tag : Tag
t : Time.From tag.time
h✝ : tag.time < t.val
⊢ tag < { time := t.val, microstep := 0 }

case inr
tag : Tag
t : Time.From tag.time
h✝ : ¬tag.time < t.val
⊢ tag < increment tag