simp [input, input.restriction, hr, ht]
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i : ID
hr : autoParam (s₁.rtr = s₂.rtr) _auto✝
ht : autoParam (s₁.tag = s₂.tag) _auto✝
⊢ input s₁ i = input s₂ i
no goals