(motive : MProd (Array Aesop.RappRef) (Array Aesop.GoalRef) → Sort u_1) →
  (r : MProd (Array Aesop.RappRef) (Array Aesop.GoalRef)) →
    ((rrefs : Array Aesop.RappRef) → (subgoals : Array Aesop.GoalRef) → motive ⟨rrefs, subgoals⟩) → motive r