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

State before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
scope scope' : SSAScope δ
⊢ equiv scope scope' → equiv scope' scope
Tactic:
intros H name τ
State after:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
scope scope' : SSAScope δ
H : equiv scope scope'
name : SSAVal
τ : MLIRType δ
⊢ get name scope' τ = get name scope τ

State before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
scope scope' : SSAScope δ
H : equiv scope scope'
name : SSAVal
τ : MLIRType δ
⊢ get name scope' τ = get name scope τ
Tactic:
specialize H name τ
State after:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
scope scope' : SSAScope δ
name : SSAVal
τ : MLIRType δ
H : get name scope τ = get name scope' τ
⊢ get name scope' τ = get name scope τ

State before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
scope scope' : SSAScope δ
name : SSAVal
τ : MLIRType δ
H : get name scope τ = get name scope' τ
⊢ get name scope' τ = get name scope τ
Tactic:
simp [H]
State after:
no goals