push_neg at h
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
t : ¬Terminal s
h : ¬(¬Closed s ∨ ∃ g, NextTag s g)
⊢ False
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
t : ¬Terminal s
h : Closed s ∧ ∀ (g : Time.Tag), ¬NextTag s g
⊢ False