∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : SizeOf Γ] [inst_1 : SizeOf Λ] [inst_2 : SizeOf σ]
  (a : Turing.Dir) (a_1 : Turing.TM1.Stmt Γ Λ σ), sizeOf (Turing.TM1.Stmt.move a a_1) = 1 + sizeOf a + sizeOf a_1