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