simp [nextTime] at ht
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
net : Network
exec : Executable net
t : Time.From (time exec)
q : Time.From exec.tag.time
ht :
  (match exec.state with
    | State.shuttingDown => none
    | State.shutdownPending =>
      some
        { val := time exec,
          property :=
            (_ :
              Nat.Linear.ExprCnstr.denote [(time exec).ns]
                { eq := false, lhs := Nat.Linear.Expr.var 0, rhs := Nat.Linear.Expr.var 0 }) }
    | State.executing => Queue.nextTime exec.queue) =
    some t
hq : Queue.nextTime exec.queue = some q
⊢ t ≤ q