{motive : Lean.Meta.Sym.CongrInfo → Sort u} →
  (t : Lean.Meta.Sym.CongrInfo) →
    motive Lean.Meta.Sym.CongrInfo.none →
      ((prefixSize suffixSize : ℕ) → motive (Lean.Meta.Sym.CongrInfo.fixedPrefix prefixSize suffixSize)) →
        ((rewritable : Array Bool) → motive (Lean.Meta.Sym.CongrInfo.interlaced rewritable)) →
          ((thm : Lean.Meta.CongrTheorem) → motive (Lean.Meta.Sym.CongrInfo.congrTheorem thm)) → motive t