[C : FP.FloatCfg] →
  {motive : FP.Float → Sort u} →
    (t : FP.Float) →
      ((a : Bool) → (e : ℤ) → (m : ℕ) → (a_1 : FP.ValidFinite e m) → motive (FP.Float.finite a e m a_1)) →
        (Nat.hasNotBit 4 t.ctorIdx → motive t) → motive t