(motive : Array (Lean.FVarId × Lean.MVarId) × Array (Lean.FVarId × Lean.MVarId) → Sort u_1) →
  (x : Array (Lean.FVarId × Lean.MVarId) × Array (Lean.FVarId × Lean.MVarId)) →
    ((active inert : Array (Lean.FVarId × Lean.MVarId)) → motive (active, inert)) → motive x