{P : Sort u} →
  {tactic tactic' : Lean.Expr} →
    Lean.Elab.Command.Structure.StructFieldDefault.autoParam tactic =
        Lean.Elab.Command.Structure.StructFieldDefault.autoParam tactic' →
      (tactic = tactic' → P) → P