simp [State.Trivial, Partial.empty_iff] at ht
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e : s₁ ↓ₛ s₂
ht : State.Trivial s₁
⊢ False
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e : s₁ ↓ₛ s₂
ht : ∀ (a : Component.idType Component.rcn), s₁.rtr[Component.rcn][a] = none
⊢ False