
postulate
  A : Set

variable
  {xx} : A

record R : Set₁ where
  field
    P : A → Set
    a : P xx
    b : P xx
    c : P xx
    d : P xx
    e : P xx
    f : P xx
    g : P xx
    h : P xx
    i : P xx
    j : P xx
    k : P xx
    l : P xx
    m : P xx
    n : P xx
    o : P xx
    p : P xx
    q : P xx
    r : P xx
    s : P xx
    t : P xx
    u : P xx
    v : P xx
    w : P xx
    x : P xx
    y : P xx
    z : P xx
