(motive : Lean.Meta.CongrArgKind → Sort u_1) →
  (x : Lean.Meta.CongrArgKind) →
    (Unit → motive Lean.Meta.CongrArgKind.fixed) →
      (Unit → motive Lean.Meta.CongrArgKind.fixedNoParam) →
        (Unit → motive Lean.Meta.CongrArgKind.eq) →
          (Unit → motive Lean.Meta.CongrArgKind.cast) →
            (Unit → motive Lean.Meta.CongrArgKind.heq) →
              (Unit → motive Lean.Meta.CongrArgKind.subsingletonInst) → motive x