simp [H1, H2]
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env₁✝ env₂✝ env₃✝ : SSAEnv δ
name : SSAVal
H1 : ∀ (τ : MLIRType δ), get name τ env₁✝ = get name τ env₂✝
H2 : ∀ (τ : MLIRType δ), get name τ env₂✝ = get name τ env₃✝
⊢ ∀ (τ : MLIRType δ), get name τ env₁✝ = get name τ env₃✝
no goals