intros H1 scope₃ H2 name τ
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
scope₁ scope₂ : SSAScope δ
⊢ equiv scope₁ scope₂ → ∀ ⦃scope₃ : SSAScope δ⦄, equiv scope₂ scope₃ → equiv scope₁ scope₃
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
scope₁ scope₂ : SSAScope δ
H1 : equiv scope₁ scope₂
scope₃ : SSAScope δ
H2 : equiv scope₂ scope₃
name : SSAVal
τ : MLIRType δ
⊢ get name scope₁ τ = get name scope₃ τ