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

Lemma iq_sys_val_cons_char {sys: ps_system} {a: tm * tm} (sol: tm):
    solves_ps_system (a::sys) sol <-> solves_ps_system sys sol /\ (fun p => (snd p) ≤b (Subst_tm (scons sol ids) (fst p))) a.
Proof.
    split.
    - intros sys_val. unfold solves_ps_system in sys_val.
    now rewrite Forall_cons_iff in sys_val.
    - intros H. now eapply Forall_cons.
Qed.

Lemma iq_sys_wf_cons_char {sys: ps_system} {a: tm * tm} (T: ty):
    ps_system_well_formed (a::sys) T <-> ps_system_well_formed sys T /\ (fun p => (cons T nil) ⊢ (fst p): Base /\ nil ⊢ (snd p): Base) a.
Proof.
    split.
    - intros sys_wf. unfold ps_system_well_formed in sys_wf.
        now rewrite Forall_cons_iff in sys_wf.
    - intros H. now eapply Forall_cons.
Qed.