{motive : Mathlib.Meta.FunProp.LambdaTheoremArgs → Sort u} →
  (t : Mathlib.Meta.FunProp.LambdaTheoremArgs) →
    ((fArgId gArgId : ℕ) → motive (Mathlib.Meta.FunProp.LambdaTheoremArgs.comp fArgId gArgId)) →
      (Nat.hasNotBit 8 t.ctorIdx → motive t) → motive t