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

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

Lemma res_ineq_sys_val_cons_char {sys: rps_system} {a: tm * bool} (sol: tm):
    solves_rps_system (a::sys) sol <-> solves_rps_system sys sol /\ ((embed (snd a)) ≤b (Subst_tm (scons sol ids) (fst a))).
Proof.
    split.
    - intros sys_sol. unfold solves_rps_system in sys_sol.
        now rewrite Forall_cons_iff in sys_sol.
    - intros H. now eapply Forall_cons.
Qed.