intros H name τ
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
scope scope' : SSAScope δ
⊢ equiv scope scope' → equiv scope' scope
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
scope scope' : SSAScope δ
H : equiv scope scope'
name : SSAVal
τ : MLIRType δ
⊢ get name scope' τ = get name scope τ