. rw [SSAEnv.getT_set_ne] <;> try assumption
  rw [SSAEnv.getT_set_ne] <;> try assumption
  intros K;
  apply Href; assumption;
case neg
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ✝ : Dialect α✝ σ✝ ε✝
env1 env2 : SSAEnv δ✝
name : SSAVal
τ : MLIRType δ✝
val : MLIRType.eval τ
Href :
  ∀ (v : SSAVal) (a : MLIRType δ✝) (b : MLIRType.eval a),
    getT v env2 = some { fst := a, snd := b } → getT v env1 = some { fst := a, snd := b }
name' : SSAVal
val' : MLIRType δ✝
Hget : MLIRType.eval val'
H : ¬name = name'
⊢ getT name' (set name τ val env2) = some { fst := val', snd := Hget } →
    getT name' (set name τ val env1) = some { fst := val', snd := Hget }
no goals