∀ {varId : Lean.FVarId} {p : Lean.Meta.Match.Pattern} {hId varId_1 : Lean.FVarId} {p_1 : Lean.Meta.Match.Pattern}
  {hId_1 : Lean.FVarId},
  Lean.Meta.Match.Pattern.as varId p hId = Lean.Meta.Match.Pattern.as varId_1 p_1 hId_1 →
    varId = varId_1 ∧ p = p_1 ∧ hId = hId_1