exact .refl _
case mut
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
cpt : Component.Valued
i : ID
x✝ : Change.Mutation
h : ¬Change.Targets (Change.mut x✝) cpt i
⊢ s₁.rtr[Component.val cpt][i] = s₁.rtr[Component.val cpt][i]
no goals