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

Notation ps_system := (list (tm * tm)).

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

Definition ps_system_solvable (sys: ps_system) (T: ty) :=
    exists sol, nil ⊢ sol : T /\ solves_ps_system sys sol.

Definition ps_system_well_formed (sys: ps_system) (T: ty) :=
    Forall (fun p => (cons T nil) ⊢ (fst p): Base /\ nil ⊢ (snd p): Base) sys.

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

Definition PS := fun p: wf_ps_system => ps_system_solvable (fst (proj1_sig p)) (snd (proj1_sig p)).