{t : Type} →
  {P : Sort u} →
    {line : Std.Http.Response.Head} →
      {body : t} →
        {extensions : Std.Http.Extensions} →
          {line' : Std.Http.Response.Head} →
            {body' : t} →
              {extensions' : Std.Http.Extensions} →
                { line := line, body := body, extensions := extensions } =
                    { line := line', body := body', extensions := extensions' } →
                  (line = line' → body ≍ body' → extensions = extensions' → P) → P