cases (env.get name τ) <;> simp at * <;> intros H1 H2 <;> subst r <;> subst env <;> simp
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
r : MLIRType.eval τ
env' : SSAEnv Δ
name' : SSAVal
Hne : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
⊢ (match SSAEnv.get name τ env with
        | some v => v
        | none => default) =
        r ∧
      env = env' →
    (match SSAEnv.get name τ env with
        | some v => v
        | none => default) =
        r ∧
      SSAEnv.set name' τ' v' env = SSAEnv.set name' τ' v' env'
no goals