From Coq Require Import List.
From PCF2.Autosubst Require Import pcf_2 unscoped.
From PCF2 Require Import CE pcf_2_system.

Notation rps_system := (list (tm * bool)).

Definition solves_rps_system (sys: rps_system) (sol: tm) :=
    Forall (fun p => (embed (snd p)) ≤b (Subst_tm (scons sol ids) (fst p))) sys.

Definition rps_system_solvable (sys: rps_system) (T: ty) :=
    exists sol, nil ⊢ sol : T /\ solves_rps_system sys sol.

Definition rps_system_well_formed (sys: rps_system) (T: ty) :=
    Forall (fun p => (cons T nil) ⊢ (fst p): Base) sys.

Definition wf_rps_system: Type := sig (fun p => match p with (sys, T) => rps_system_well_formed sys T end).

Definition RPS := fun p: wf_rps_system => rps_system_solvable (fst (proj1_sig p)) (snd (proj1_sig p)).