{P : Sort u} →
  {pattern : Lean.Meta.Sym.Pattern} →
    {unify zetaDelta : Bool} →
      {pattern' : Lean.Meta.Sym.Pattern} →
        {unify' zetaDelta' : Bool} →
          { pattern := pattern, unify := unify, zetaDelta := zetaDelta } =
              { pattern := pattern', unify := unify', zetaDelta := zetaDelta' } →
            (pattern = pattern' → unify = unify' → zetaDelta = zetaDelta' → P) → P