intro ht hq
net : Network
exec : Executable net
t : Time.From (time exec)
q : Time.From exec.tag.time
⊢ nextTime exec = some t → Queue.nextTime exec.queue = some q → t ≤ q
net : Network
exec : Executable net
t : Time.From (time exec)
q : Time.From exec.tag.time
ht : nextTime exec = some t
hq : Queue.nextTime exec.queue = some q
⊢ t ≤ q