subst rEnv
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') → env' = env
env : SSAEnv Δ
r✝ : List (TypedArg Δ)
env' : SSAEnv Δ
headName : SSAVal
headτ : MLIRType Δ
r : MLIRType.eval headτ × SSAEnv Δ
rRes : MLIRType.eval headτ
rEnv : SSAEnv Δ
H :
  (match
      mapM
        (fun x s =>
          match TopM.get x.snd x.fst s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
        tail (rRes, rEnv).snd with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := (rRes, rEnv).fst } :: v.fst, v.snd)) =
    Except.ok (r✝, env')
left✝ :
  (match SSAEnv.get headName headτ env with
    | some v => v
    | none => default) =
    rRes
right✝ : env = rEnv
⊢ env' = env
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') → env' = env
env : SSAEnv Δ
r✝ : List (TypedArg Δ)
env' : SSAEnv Δ
headName : SSAVal
headτ : MLIRType Δ
r : MLIRType.eval headτ × SSAEnv Δ
rRes : MLIRType.eval headτ
left✝ :
  (match SSAEnv.get headName headτ env with
    | some v => v
    | none => default) =
    rRes
H :
  (match
      mapM
        (fun x s =>
          match TopM.get x.snd x.fst s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
        tail (rRes, env).snd with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := (rRes, env).fst } :: v.fst, v.snd)) =
    Except.ok (r✝, env')
⊢ env' = env