Increment counter by 1 in ghost state

DataflowRewriter/Rewrites/LoopRewriteCorrect.lean

@@ -211,7 +211,10 @@ Essentially tagger + join without internal rule
 @[drunfold] def StringModule.tagger_untagger_val_ghost TagT [DecidableEq TagT] T :=
   NatModule.tagger_untagger_val_ghost TagT T |>.stringify
 
-def liftF2 {α β γ δ} (f : α -> β × δ) : α × γ -> (β × γ) × δ | (a, g) => ((f a |>.fst, g), f a |>.snd)
+def liftF2 {α β γ δ} (f : α -> β × δ) : α × (Nat × γ) -> (β × (Nat × γ)) × δ
+| (a, g) =>
+  let b := f a
+  ((b.1, (g.1 + 1, g.2)), b.2)
 
 def ghost_rhs
     : ExprHigh String × IdentMap String (TModule1 String) := [graphEnv|