[C : FP.FloatCfg] →
  (motive : FP.Float → FP.Float → Sort u_1) →
    (x x_1 : FP.Float) →
      ((x : FP.Float) → motive FP.Float.nan x) →
        ((x : FP.Float) → motive x FP.Float.nan) →
          ((s₁ : Bool) → (f₂ : FP.Float) → motive (FP.Float.inf s₁) f₂) →
            ((f₁ : FP.Float) → (s₂ : Bool) → motive f₁ (FP.Float.inf s₂)) →
              ((s₁ : Bool) →
                  (e₁ : ℤ) →
                    (m₁ : ℕ) →
                      (v₁ : FP.ValidFinite e₁ m₁) →
                        (s₂ : Bool) →
                          (e₂ : ℤ) →
                            (m₂ : ℕ) →
                              (v₂ : FP.ValidFinite e₂ m₂) →
                                motive (FP.Float.finite s₁ e₁ m₁ v₁) (FP.Float.finite s₂ e₂ m₂ v₂)) →
                motive x x_1