rw [transpose_involutive]
t1 : RankedTensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32
⊢ [(SSAVal.SSAVal "t1",
        { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32), snd := t1 }),
      (SSAVal.SSAVal "t2",
        {
          fst :=
            MLIRType.extended
              (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)),
          snd := transpose t1 }),
      (SSAVal.SSAVal "t3",
        {
          fst :=
            MLIRType.extended
              (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] (MLIRType.int Signedness.Signless 32)),
          snd := transpose (transpose t1) })] =
    [(SSAVal.SSAVal "t1",
        { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32), snd := t1 }),
      (SSAVal.SSAVal "t2",
        { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] MLIRType.i32),
          snd := transpose t1 }),
      (SSAVal.SSAVal "t3",
        { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32), snd := t1 })]
no goals