simp[LHS, RHS]
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 })])
r✝ : Region linalg
t : Tensor1D
r : Region linalg
rSpec : ℤ → FinInt 32 → FinInt 32
valid_r : validGenericRegion r rSpec
⊢ run
      (denoteRegion linalg
        (Region.mk "entry" []
          [Op.mk "linalg.generic1d" [(SSAVal.SSAVal "x", MLIRType.tensor1d)] [(SSAVal.SSAVal "t", MLIRType.tensor1d)]
              [r] (AttrDict.mk [AttrEntry.mk "len" (AttrValue.int 10 MLIRType.index)]),
            Op.mk "linalg.fill1d" [(SSAVal.SSAVal "out", MLIRType.tensor1d)] [(SSAVal.SSAVal "x", MLIRType.tensor1d)] []
              (AttrDict.mk [AttrEntry.mk "cst" (AttrValue.int 42 MLIRType.index)])])
        [])
      (SSAEnv.One [(SSAVal.SSAVal "t", { fst := MLIRType.tensor1d, snd := t })]) =
    run
      (denoteRegion linalg
        (Region.mk "entry" []
          [Op.mk "linalg.generic1d" [(SSAVal.SSAVal "x", MLIRType.tensor1d)] [(SSAVal.SSAVal "t", MLIRType.tensor1d)]
              [r] (AttrDict.mk [AttrEntry.mk "cst" (AttrValue.int 42 MLIRType.index)]),
            Op.mk "linalg.extractslice1d" [(SSAVal.SSAVal "out", MLIRType.tensor1d)]
              [(SSAVal.SSAVal "x", MLIRType.tensor1d)] []
              (AttrDict.mk [AttrEntry.mk "len" (AttrValue.int 10 MLIRType.index)])])
        [])
      (SSAEnv.One [(SSAVal.SSAVal "t", { fst := MLIRType.tensor1d, snd := t })])