{P : Sort u} →
  {name : Lean.Name} →
    {symm : Bool} →
      {name' : Lean.Name} →
        {symm' : Bool} →
          { name := name, symm := symm } = { name := name', symm := symm' } → (name = name' → symm = symm' → P) → P