Fixpoint W (p : prp) : Type :=
  match p with
    | atm p => unit
    | pls p1 p2 => W p1 + W p2
    | tns p1 p2 => W p1 * W p2
    | bng p => W p
    | opp p => C p
    | unv ty p' => forall x : ty, W (p' x)
  end

with C p :=
  match p with
    | atm p => ctx
    | pls p1 p2 => C p1 * C p2
    | tns p1 p2 => (W p1 -> C p2) * (W p2 -> C p1)
    | bng p => Rlist.t (W p) (C p)
    | opp p => W p
    | unv ty p' => { x : ty & C (p' x) }
  end.