intros H name
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env env' : SSAEnv δ
⊢ equiv env env' → equiv env' env
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env env' : SSAEnv δ
H : equiv env env'
name : SSAVal
⊢ ∀ (τ : MLIRType δ), get name τ env' = get name τ env