simp_itree
t1 : RankedTensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32
⊢ (Fitree.bind
      (ToyOp.handle (RankedTensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32))
        (ToyOp.Transpose (MLIRType.int Signedness.Signless 32) 2 4 t1))
      fun x =>
      Fitree.bind
        (ToyOp.handle (RankedTensor [Dimension.Known 2, Dimension.Known 4] (MLIRType.int Signedness.Signless 32))
          (ToyOp.Transpose (MLIRType.int Signedness.Signless 32) 4 2 x))
        fun x_1 =>
        Fitree.ret
          ((),
            SSAEnv.One
              [(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 := x }),
                (SSAVal.SSAVal "t3",
                  {
                    fst :=
                      MLIRType.extended
                        (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] (MLIRType.int Signedness.Signless 32)),
                    snd := x_1 })])) =
    Fitree.Ret
      ((),
        SSAEnv.One
          [(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 })])
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 })]