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

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

State before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
scope : SSAScope δ
name : SSAVal
τ : MLIRType δ
⊢ get name scope τ = get name scope τ
Tactic:
rfl
State after:
no goals