intros HEnv name τ v name' τ'
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env₁ env₂ : SSAEnv δ
⊢ equiv env₁ env₂ →
    ∀ ⦃name : SSAVal⦄ ⦃τ : MLIRType δ⦄ ⦃v : MLIRType.eval τ⦄, equiv (set name τ v env₁) (set name τ v env₂)
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env₁ env₂ : SSAEnv δ
HEnv : equiv env₁ env₂
name : SSAVal
τ : MLIRType δ
v : MLIRType.eval τ
name' : SSAVal
τ' : MLIRType δ
⊢ get name' τ' (set name τ v env₁) = get name' τ' (set name τ v env₂)