∀ (masks : List (Array Bool)) (mask : Array Bool) (i : ℕ) (type : Lean.Expr) (typesToCheck : List Lean.Expr),
  Lean.Elab.Command.fixedIndicesToParams.go✝ masks mask i type typesToCheck =
    if i < mask.size then
      have __do_jp := fun y =>
        have __do_jp := fun y =>
          have paramType := type.bindingDomain!;
          do
          let __do_lift ← List.allM (fun type => Lean.Elab.Command.isDomainDefEq✝ type paramType) typesToCheck
          have __do_jp : PUnit.{1} → Lean.MetaM ℕ := fun y =>
            Lean.Meta.withLocalDeclD `a paramType fun paramNew => do
              let typesToCheck ←
                List.mapM (fun type => Lean.Meta.whnfD (type.bindingBody!.instantiate1 paramNew)) typesToCheck
              Lean.Elab.Command.fixedIndicesToParams.go✝¹ masks mask (i + 1) (type.bindingBody!.instantiate1 paramNew)
                  typesToCheck
          if (!__do_lift) = true then
              have cls := `Elab.inductive;
              do
              let __do_lift ← Lean.isTracingEnabledFor cls
              have __do_jp : Unit → Lean.MetaM ℕ := fun y => pure i
              if __do_lift = true then do
                  let y ←
                    Lean.addTrace cls
                        (Lean.toMessageData "domain not def eq: " ++ Lean.toMessageData i ++ Lean.toMessageData ", " ++
                              Lean.toMessageData type ++
                            Lean.toMessageData " =?= " ++
                          Lean.toMessageData paramType)
                  __do_jp y
                else do
                  let y ← pure PUnit.unit
                  __do_jp y
            else do
              let y ← pure PUnit.unit
              __do_jp y;
        if (!type.isForall) = true then pure i
        else do
          let y ← pure PUnit.unit
          __do_jp y;
      if (!masks.all fun mask => decide (i < mask.size) && mask[i]!) = true then pure i
      else do
        let y ← pure PUnit.unit
        __do_jp y
    else pure i