(motive : Lean.MVarId × Array Lean.FVarId → Sort u_1) →
  (__discr : Lean.MVarId × Array Lean.FVarId) →
    ((goal' : Lean.MVarId) → (removedFVars : Array Lean.FVarId) → motive (goal', removedFVars)) → motive __discr