intros t1
⊢ ∀ (t1 : RankedTensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
    run_toy (toy_semantics_region double_transpose)
        (SSAEnv.One
          [(SSAVal.SSAVal "t1",
              { fst := builtin.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32, snd := t1 })]) =
      Fitree.ret
        ((),
          SSAEnv.One
            [(SSAVal.SSAVal "t1",
                { fst := builtin.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32, snd := t1 }),
              (SSAVal.SSAVal "t2",
                { fst := builtin.tensor [Dimension.Known 4, Dimension.Known 2] MLIRType.i32, snd := transpose t1 }),
              (SSAVal.SSAVal "t3",
                { fst := builtin.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32, snd := t1 })])
t1 : RankedTensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32
⊢ run_toy (toy_semantics_region double_transpose)
      (SSAEnv.One
        [(SSAVal.SSAVal "t1",
            { fst := builtin.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32, snd := t1 })]) =
    Fitree.ret
      ((),
        SSAEnv.One
          [(SSAVal.SSAVal "t1",
              { fst := builtin.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32, snd := t1 }),
            (SSAVal.SSAVal "t2",
              { fst := builtin.tensor [Dimension.Known 4, Dimension.Known 2] MLIRType.i32, snd := transpose t1 }),
            (SSAVal.SSAVal "t3",
              { fst := builtin.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32, snd := t1 })])