intros valid_r
r✝ : Region linalg
t : Tensor1D
r : Region linalg
rSpec : ℤ → FinInt 32 → FinInt 32
⊢ validGenericRegion r rSpec →
    run ⟦ LHS r ⟧ (SSAEnv.One [(SSAVal.SSAVal "t", { fst := MLIRType.tensor1d, snd := t })]) =
      run ⟦ RHS r ⟧ (SSAEnv.One [(SSAVal.SSAVal "t", { fst := MLIRType.tensor1d, snd := t })])
r✝ : Region linalg
t : Tensor1D
r : Region linalg
rSpec : ℤ → FinInt 32 → FinInt 32
valid_r : validGenericRegion r rSpec
⊢ run ⟦ LHS r ⟧ (SSAEnv.One [(SSAVal.SSAVal "t", { fst := MLIRType.tensor1d, snd := t })]) =
    run ⟦ RHS r ⟧ (SSAEnv.One [(SSAVal.SSAVal "t", { fst := MLIRType.tensor1d, snd := t })])