exact q.property
case h_2
net : Network
exec : Executable net
t : Time.From (time exec)
q : Time.From exec.tag.time
x✝ : State
hq : Queue.nextTime exec.queue = some q
heq✝ : exec.state = State.shutdownPending
ht :
  { 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 }) } =
    t
⊢ { 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 }) } ≤
    q
no goals