simp [H1, H2]
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
scope₁ scope₂ scope₃ : SSAScope δ
name : SSAVal
τ : MLIRType δ
H1 : get name scope₁ τ = get name scope₂ τ
H2 : get name scope₂ τ = get name scope₃ τ
⊢ get name scope₁ τ = get name scope₃ τ
no goals