∀ (masks : List (Array Bool)) (mask : Array Bool) (_x : (_ : ℕ) ×' (_ : Lean.Expr) ×' List Lean.Expr),
  Lean.Elab.Command.fixedIndicesToParams.go._unary✝ masks mask _x =
    PSigma.casesOn _x fun i type =>
      PSigma.casesOn type fun 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._unary✝¹ 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