{α : Sort u} →
  {motive : Plausible.SampleableExt α → Sort u_1} →
    ((proxy : Type v) →
        [proxyRepr : Repr proxy] →
          [shrink : Plausible.Shrinkable proxy] →
            [sample : Plausible.Arbitrary proxy] →
              (interp : proxy → α) →
                motive
                  { proxy := proxy, proxyRepr := proxyRepr, shrink := shrink, sample := sample, interp := interp }) →
      (t : Plausible.SampleableExt α) → motive t