∀ {V : Type u_11} {E : Type u_12} [inst : LineDeriv V E E] {n : ℕ} (m : Fin (n + 1) → V) (f : E),
  LineDeriv.iteratedLineDerivOp m f = LineDeriv.lineDerivOp (m 0) (LineDeriv.iteratedLineDerivOp (Fin.tail m) f)