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

State before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env : SSAEnv δ
⊢ equiv env env
Tactic:
intros v τ
State after:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env : SSAEnv δ
v : SSAVal
τ : MLIRType δ
⊢ get v τ env = get v τ env

State before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env : SSAEnv δ
v : SSAVal
τ : MLIRType δ
⊢ get v τ env = get v τ env
Tactic:
rfl
State after:
no goals