Theorem: SSAEnv.equiv_symm (MLIR/Semantics/SSAEnv.lean)

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

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

State before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env env' : SSAEnv δ
name : SSAVal
H : ∀ (τ : MLIRType δ), get name τ env = get name τ env'
⊢ ∀ (τ : MLIRType δ), get name τ env' = get name τ env
Tactic:
simp [H]
State after:
no goals