Theorem: denoteTypedArgs_cons_unfold (MLIR/Semantics/Semantics.lean)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
headVal : SSAVal
tailVal : List SSAVal
headArgs : TypedArg Δ
tailArgs : List (TypedArg Δ)
env : SSAEnv Δ
⊢ denoteTypedArgs (headArgs :: tailArgs) (headVal :: tailVal) env =
    bind (TopM.set headArgs.fst headVal headArgs.snd) (fun x => denoteTypedArgs tailArgs tailVal) env
Tactic:
simp [denoteTypedArgs]
State after:
no goals