{K : Type u_1} →
  (motive : Option (GenContFract.Pair K) × Option (GenContFract.Pair K) → Sort u_2) →
    (x : Option (GenContFract.Pair K) × Option (GenContFract.Pair K)) →
      ((gp_n gp_succ_n : GenContFract.Pair K) → motive (some gp_n, some gp_succ_n)) →
        ((x : Option (GenContFract.Pair K) × Option (GenContFract.Pair K)) →
            (∀ (gp_n gp_succ_n : GenContFract.Pair K), x = (some gp_n, some gp_succ_n) → False) → motive x) →
          motive x