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

State before:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v : SSAVal
env : SSAEnv δ
τ : MLIRType δ
val : MLIRType.eval τ
⊢ get v τ (set v τ val env) = some val
Tactic:
simp [get, getT_set_eq]
State after:
no goals