ITree.Extra.Secure.SecureEqEuttHalt

From Coq Require Import Morphisms.

From ITree Require Import
     Axioms
     ITree
     ITreeFacts.

From ITree.Extra Require Import
     Secure.Labels
     Secure.SecureEqHalt
.

From Paco Require Import paco.

Import Monads.
Import MonadNotation.
Local Open Scope monad_scope.

Lemma tau_eqit_secure : E R1 R2 Label priv l RR (t1 : itree E ) (t2 : itree E ),
    eqit_secure Label priv RR true true l (Tau ) eqit_secure Label priv RR true true l .
Proof.
  intros E Label priv l RR. intros Hsec. pstep. red.
  punfold Hsec. red in Hsec. cbn in ×. remember (TauF ) as x.
  hinduction Hsec before priv; intros; inv Heqx; pclearbot; try inv CHECK; auto with itree.
  - constructor; auto. pstep_reverse.
  - unpriv_ind. pstep_reverse.
  - punfold H.
Qed.


Lemma unpriv_e_eqit_secure : E A R1 R2 Label priv l RR (e : E A) (k : A itree E )
      (t : itree E ),
    (¬leq (priv A e) l )
    eqit_secure Label priv RR true true l (Vis e k) t
     a, eqit_secure Label priv RR true true l (k a) t.
Proof.
  intros. generalize dependent t. rename H into Hunpriv. generalize dependent a.
  intros. punfold . red in . cbn in ×. pfold. red.
  remember (VisF e k) as x. genobs_clear t ot.
  hinduction before l; intros; try inv Heqx;
    ddestruction; subst; try contradiction; try contra_size; auto.
  - constructor; auto. eapply IHsecure_eqitF; eauto.
  - pclearbot. constructor; auto. pstep_reverse.
  - unpriv_ind. pstep_reverse. pclearbot. apply H.
  - unpriv_ind. eapply ; eauto.
  - pclearbot. rewrite itree_eta'. pstep_reverse.
Qed.


(* reformat this lemma? useful but unclear *)
Lemma eses_aux1: (E : Type Type) (R2 R1 : Type) (Label : Preorder)
                    (priv : A : Type, E A L) (l : L) (RR : Prop)
                    (r : itree E itree E Prop) (m1 m2 : itree E ),
              
               ( (t1 t1' : itree E ) (t2 : itree E ),
                    eqit_secure Label priv RR true true l r )
                (X : Type) (e : E X) (k : X itree E ),
                 secure_eqitF Label priv RR true true l id
                              ( (secure_eqit_ Label priv RR true true l id) ) (observe )
                              (VisF e k)
                 leq (priv X e) l
                 secure_eqitF Label priv RR true true l id
                              ( (secure_eqit_ Label priv RR true true l id) r) (observe )
                              (VisF e k).
Proof.
  intros E Label priv l RR r REL CIH X e k Hsec SECCHECK.
  remember (VisF e k) as x. punfold REL. red in REL. rewrite Heqx.
  hinduction Hsec before r; intros; try inv Heqx; ddestruction; subst; try contradiction; auto.
  - eapply IHHsec; eauto.
    pstep_reverse. setoid_rewrite tau_eutt at 1. pfold. auto.
  - pclearbot. remember (VisF ) as y.
    hinduction REL before r; intros; try inv Heqy; ddestruction; subst; auto.
    + constructor; auto. right. eapply CIH; eauto; try apply H.
      pclearbot. apply REL.
    + constructor; eauto.
  - rewrite . remember (VisF e ) as y.
    hinduction REL before r; intros; try inv Heqy; ddestruction; subst; auto.
    + pclearbot. rewrite . unpriv_ind. rewrite . eapply ; eauto.
      Unshelve. all: auto. pstep_reverse.
    + constructor; auto. eapply IHREL; eauto.
Qed.


Lemma eses_aux2:
(E : Type Type) (R2 R1 : Type) (Label : Preorder)
    (priv : A : Type, E A L) (l : L) (RR : Prop)
    (r : itree E itree E Prop) (m1 m2 : itree E ) (r0 : ),
  
  secure_eqitF Label priv RR true true l id
    ( (secure_eqit_ Label priv RR true true l id) ) (observe )
    (RetF )
  secure_eqitF Label priv RR true true l id
    ( (secure_eqit_ Label priv RR true true l id) r) (observe )
    (RetF ).
Proof.
  intros E Label priv l RR r Heutt Hsec.
  punfold Heutt. red in Heutt. remember (RetF ) as x.
  rewrite Heqx. hinduction Hsec before r; intros; inv Heqx; auto with itree.
  - remember (RetF ) as y.
    hinduction Heutt before r; intros; inv Heqy; auto with itree.
    constructor; auto. eapply IHHeutt; eauto.
  - eapply IHHsec; eauto. pstep_reverse. rewrite tau_eutt at 1. pfold. auto.
  - remember (VisF e ) as y.
    hinduction Heutt before r; intros; inv Heqy; ddestruction; subst; auto.
    + unpriv_ind. rewrite . eapply ; eauto.
       pclearbot. pstep_reverse.
    + constructor; auto. eapply IHHeutt; eauto.
Qed.


Definition classic_empty := Secure.Labels.classic_empty.

(*tomorrow start on the transitivity proof *)
Lemma eutt_secure_eqit_secure : E Label priv l R1 R2 RR (t1 t1': itree E ) (t2 : itree E ),
     eqit_secure Label priv RR true true l
    eqit_secure Label priv RR true true l .
Proof.
  intros E Label priv l RR. pcofix CIH. intros Heutt Hsec.
  punfold Heutt. red in Heutt. punfold Hsec. red in Hsec.
  pfold. red. hinduction Heutt before r; intros; subst; auto with itree.
  - remember (RetF ) as x. hinduction Hsec before r; intros; try inv Heqx; auto with itree.
    + constructor; auto. eapply IHHsec; eauto.
    + unpriv_ind. eapply ; eauto.
  - genobs_clear .
    assert ( : ( m3, = TauF ) ( m3, TauF ) ).
    { destruct ; eauto; right; repeat intro; discriminate. }
    (* because of the extra inductive cases this is not enough *)
    destruct as [ [ ] | ].
    + subst. pclearbot. constructor. right. eapply CIH; eauto.
      apply tau_eqit_secure. apply eqit_secure_sym. apply tau_eqit_secure.
      apply eqit_secure_sym. pfold. auto.
    + destruct ; try (exfalso; eapply ; eauto; fail).
      × pclearbot. rewrite itree_eta' at 1. eapply eses_aux2 with ( := Tau ); eauto.
        do 2 rewrite tau_eutt. auto.
      × assert (leq (priv _ e) l ¬ leq (priv _ e) l).
        { apply classic. }
        destruct H as [SECCHECK | SECCHECK]; destruct ( classic_empty X ).
        ++ pclearbot. rewrite itree_eta' at 1. apply eses_aux1 with ( := Tau ); auto.
           do 2 rewrite tau_eutt. auto.
        ++ pclearbot. rewrite itree_eta' at 1. apply eses_aux1 with ( := Tau ); auto.
           do 2 rewrite tau_eutt. auto.
        ++ unpriv_halt. pclearbot. right. eapply CIH; eauto.
           apply tau_eqit_secure. pfold. auto.
        ++ pclearbot.
           unpriv_co. pclearbot. right. eapply CIH. apply REL.
           apply tau_eqit_secure.
           apply eqit_secure_sym.
           eapply unpriv_e_eqit_secure; eauto.
           apply eqit_secure_sym. pfold. auto.
  - pclearbot. rewrite itree_eta' at 1. pstep_reverse.
    assert (eqit_secure Label priv RR true true l (Vis e ) ).
    { pfold; auto. }
    clear Hsec. rename H into Hsec.
    destruct (classic (leq (priv _ e) l ) ).
    + pstep. red. punfold Hsec. red in Hsec.
      cbn in ×. remember (VisF e ) as x.
      hinduction Hsec before r; intros; inv Heqx; ddestruction; subst; try contradiction; auto.
      × constructor; auto. eapply IHHsec; eauto.
      × constructor; auto; intros. right. eapply CIH; try apply REL. pclearbot. apply H.
      × rewrite itree_eta' at 1. unpriv_ind. eapply ; eauto.
    + destruct (classic_empty u).
      × pfold. red. cbn. punfold Hsec. red in Hsec. cbn in ×.
        destruct (observe ).
        -- inv Hsec; contra_size.
        -- unpriv_halt. right. apply CIH with ( := Vis e ).
           ++ pfold. constructor. left. auto.
           ++ inv Hsec; ddestruction; subst; try contradiction; try contra_size. pfold. auto.
              pclearbot. auto.
        -- inv Hsec; ddestruction; subst; try contradiction; try contra_size.
           ++ unpriv_halt. right. apply CIH with ( := Vis e ).
              { pfold. constructor. red. auto. }
              { rewrite in . pfold. apply . }
           ++ pclearbot. unpriv_halt. right. apply CIH with ( := Vis e ).
              { pfold. constructor. red. auto. }
              { apply . }
           ++ pclearbot. unpriv_halt. contra_size.
      × pfold. red. cbn. punfold Hsec. red in Hsec. cbn in ×.
        destruct (observe ).
        ++ rewrite itree_eta' at 1. rewrite itree_eta' in Hsec at 1.
           eapply eses_aux2; eauto. pfold. constructor. red. auto.
        ++ unpriv_co. right. apply CIH with ( := a); try apply REL.
           eapply unpriv_e_eqit_secure; eauto. apply eqit_secure_sym.
           apply tau_eqit_secure. apply eqit_secure_sym. pfold. auto.
        ++ destruct (classic (leq (priv _ ) l )).
           ** rewrite itree_eta' at 1.
              eapply eses_aux1 with ( := Vis e ); eauto.
              pfold. constructor. red. auto.
           ** destruct (classic_empty X).
              --- unpriv_halt. right. eapply CIH; try apply REL.
                  eapply unpriv_e_eqit_secure; eauto. pfold. auto.
              --- unpriv_co. right. eapply CIH; try apply REL.
                  (* eapply unpriv_e_eqit_secure; eauto. *)
                  do 2 (eapply unpriv_e_eqit_secure; eauto; apply eqit_secure_sym).
                  pfold. auto.
  - eapply IHHeutt; eauto. pstep_reverse.
    apply tau_eqit_secure. pfold. auto.
Qed.


Lemma eqit_secure_TauLR :
   (E : Type Type) (R3 : Type) (Label : Preorder) (priv : x : Type, E x L)
    (l : L) (b1 b2 : bool) (R2 : Type) (RR2 : Prop) (t0 : itree E )
    (t4 : itree E ),
    eqit_secure Label priv l (Tau ) (Tau )
    eqit_secure Label priv l .
Proof.
  intros E Label priv l .
  intros. punfold H. red in H. cbn in ×. pstep. red.
  remember (TauF ) as x. remember (TauF ) as y.
  hinduction H before ; intros; try discriminate.
  - inv Heqx; inv Heqy. pclearbot. pstep_reverse.
  - inv Heqx. inv H; eauto with itree.
    + pclearbot. unpriv_ind. pstep_reverse.
    + unpriv_ind. rewrite in .
      specialize ( a). genobs ( a) . clear .
      remember (TauF ) as y.
      hinduction before ; intros; inv Heqy; try inv CHECK; eauto with itree.
      × pclearbot. constructor; auto; pstep_reverse.
      × pclearbot. unpriv_ind. pstep_reverse.
      × pclearbot. punfold H.
    + pclearbot. punfold .
  - inv Heqy. inv H; eauto with itree.
    + pclearbot. unpriv_ind. pstep_reverse.
    + rewrite in . unpriv_ind. specialize ( a).
      genobs ( a) . clear .
      remember (TauF ) as y.
      hinduction before ; intros; inv Heqy; try inv CHECK; eauto with itree.
      × pclearbot. constructor; auto. pstep_reverse.
      × unpriv_ind. pclearbot. pstep_reverse.
      × pclearbot. punfold H.
    + pclearbot. punfold .
Qed.


Lemma eqit_secure_TauLVisR:
   (E : Type Type) (R3 : Type) (Label : Preorder) (priv : x : Type, E x L)
    (l : L) (b1 b2 : bool) (R2 : Type) (RR2 : Prop),
     (t3 : itree E ) (X : Type) (e : E X) (k : X itree E ) (a : X),
      (¬ leq (priv _ e) l)
      eqit_secure Label priv l (Tau ) (Vis e k)
      eqit_secure Label priv l (k a).
Proof.
  intros E Label priv l RR A e k a He Hsec.
  punfold Hsec. red in Hsec. cbn in ×.
  remember (TauF ) as x. remember (VisF e k) as y.
  hinduction Hsec before ; intros; try discriminate.
  - inv Heqx. inv CHECK.
    remember (VisF e k) as y. pfold. red. clear IHHsec.
    hinduction Hsec before ; intros; inv Heqy; ddestruction; subst;
    try contradiction; try contra_size; eauto with itree.
    + constructor; auto. pclearbot. pstep_reverse.
    + unpriv_ind. pclearbot. pstep_reverse.
    + pclearbot. specialize (H a). punfold H.
  - inv Heqx. inv Heqy. ddestruction; subst. pclearbot. apply H.
  - inv Heqx. inv Heqy. ddestruction; subst. rewrite in H.
    clear . clear . remember (TauF ) as x.
    pfold. red. specialize (H a).
    hinduction H before ; intros; inv Heqx; try contra_size; eauto with itree.
    + pclearbot. constructor; auto. pstep_reverse.
    + pclearbot. unpriv_ind. pstep_reverse.
    + pclearbot. punfold H.
  - pclearbot. inv Heqx. inv Heqy. ddestruction; subst. contra_size.
Qed.


Lemma eqit_secure_TauRVisL:
   (E : Type Type) (R3 : Type) (Label : Preorder) (priv : x : Type, E x L)
    (l : L) (b1 b2 : bool) (R2 : Type) RR2,
     (t3 : itree E ) (X : Type) (e : E X) (k : X itree E ) (a : X),
      (¬ leq (priv _ e) l)
      eqit_secure Label priv l (Vis e k) (Tau )
      eqit_secure Label priv l (k a) .
Proof.
  intros E Label priv l RR A e k a He Hsec.
  punfold Hsec. red in Hsec. cbn in ×.
  remember (TauF ) as x. remember (VisF e k) as y.
  hinduction Hsec before ; intros; try discriminate.
  - inv Heqx. inv CHECK. remember (VisF e k) as y. pfold. red. clear IHHsec.
    hinduction Hsec before ; intros; inv Heqy; ddestruction; subst;
    try contradiction; eauto with itree.
    + constructor; auto with itree. pclearbot. pstep_reverse.
    + unpriv_ind. pclearbot. pstep_reverse.
    + contra_size.
    + contra_size.
    + pclearbot. specialize (H a). punfold H.
  - inv Heqx. inv Heqy. ddestruction; subst. pclearbot. apply H.
  - inv Heqx. inv Heqy. ddestruction; subst. pclearbot. rewrite in H. inv CHECK.
    specialize (H a). pfold. red. remember (TauF ) as y.
    hinduction H before ; intros; inv Heqy; try contra_size; eauto with itree.
    + pclearbot. constructor; auto. pstep_reverse.
    + pclearbot. unpriv_ind. pstep_reverse.
    + pclearbot. punfold H.
  - inv Heqx. inv Heqy. ddestruction; subst. contra_size.
Qed.


Lemma eqit_secure_VisLR:
   (E : Type Type) (R3 : Type) (Label : Preorder) (priv : x : Type, E x L)
    (l : L) (b1 b2 : bool) (R2 : Type) (RR2 : Prop) (A : Type)
    (e : E A) (k2 : A itree E ),
    ¬ leq (priv A e) l
     (X : Type) (e0 : E X) (k : X itree E ) (a : A),
      ¬ leq (priv X ) l
       a0 : X,
        eqit_secure Label priv l (Vis e ) (Vis k)
        eqit_secure Label priv l ( a) (k ).
Proof.
  intros E Label priv l A e SECCHECK X k a .
  pfold. red.
  punfold . red in . cbn in ×. remember (VisF e ) as x.
  remember (VisF k) as y.
  hinduction before l; intros; try discriminate.
  - inv Heqx. inv Heqy. ddestruction; subst. contradiction.
  - pclearbot. inv Heqx. inv Heqy. ddestruction; subst. pstep_reverse.
  - inv Heqx. ddestruction; subst. inv CHECK. clear .
    specialize (H a).
    rewrite Heqy in H. clear Heqy. remember (VisF k) as y.
    hinduction H before l; intros; inv Heqy; ddestruction; subst; try contradiction;
    try contra_size; eauto with itree.
    + pclearbot. constructor; auto. pstep_reverse.
    + unpriv_ind. pclearbot. pstep_reverse.
    + pclearbot. specialize (H ). punfold H.

  - inv Heqy. ddestruction; subst. inv CHECK. clear .
    rewrite Heqx in H. specialize (H ).
    remember (VisF ) as y.
    hinduction H before ; intros; inv Heqy; ddestruction; subst; try contradiction;
    try contra_size; eauto with itree.
    + pclearbot. constructor; auto. pstep_reverse.
    + pclearbot. unpriv_ind. pstep_reverse.
    + pclearbot. specialize (H a). punfold H.
  - inv Heqx; inv Heqy; ddestruction; subst. contra_size.
  - inv Heqx; inv Heqy; ddestruction; subst. contra_size.
Qed.


Lemma eqit_secure_private_VisLR:
   (E : Type Type) (R3 : Type) (Label : Preorder) (priv : x : Type, E x L)
    (l : L) (b1 b2 : bool) (R2 : Type) (RR2 : Prop) (A : Type)
    (e : E A) (k2 : A itree E ),
    nonempty A
    ¬ leq (priv A e) l
     (X : Type) (e0 : E X) (k : X itree E ),
      ¬ leq (priv X ) l
      nonempty X
      ( a a0,
        eqit_secure Label priv l ( a) (k ))
        eqit_secure Label priv l (Vis e ) (Vis k) .
Proof.
  intros. pfold. red. cbn. unpriv_co. left. apply .
Qed.


Lemma eqit_secure_private_VisL:
   (E : Type Type) (R3 : Type) (Label : Preorder) (priv : x : Type, E x L)
    (l : L) (b2 : bool) (R2 : Type) (RR2 : Prop) (A : Type)
    (e : E A) (k2 : A itree E ) (t : itree E ),
    nonempty A
    ¬ leq (priv A e) l
    ( a,
        eqit_secure Label priv true l ( a) t)
        eqit_secure Label priv true l (Vis e ) t .
Proof.
  intros. pfold. red. cbn. unpriv_ind. pstep_reverse. apply .
Qed.


Lemma eqit_secure_private_VisR:
   (E : Type Type) (R3 : Type) (Label : Preorder) (priv : x : Type, E x L)
    (l : L) (b1 : bool) (R2 : Type) (RR2 : Prop) (A : Type)
    (e : E A) (k2 : A itree E ) (t : itree E ),
    nonempty A
    ¬ leq (priv A e) l
    ( a,
        eqit_secure Label priv true l t ( a))
        eqit_secure Label priv true l t (Vis e ).
Proof.
  intros. pfold. red. cbn. unpriv_ind. pstep_reverse. apply .
Qed.


Lemma eqit_secure_public_Vis : (E : Type Type) (R1 R2 : Type) (Label : Preorder) (priv : x : Type, E x L)
    (l : L) (b1 b2 : bool) (RR : Prop) (A : Type)
    (e : E A) (k1: A itree E ) (k2 : A itree E ),
    leq (priv A e) l
    (eqit_secure Label priv RR l (Vis e ) (Vis e )
     a, eqit_secure Label priv RR l ( a) ( a)).
Proof.
  split; intros.
  - pinversion ; ddestruction; subst; try contradiction; apply .
  - pfold. constructor; auto. left. apply .
Qed.


Lemma eqit_secure_trans_aux1:
   (E : Type Type) (R3 R1 : Type) (Label : Preorder)
    (priv : x : Type, E x L) (l : L) (b2 : bool) (R2 : Type)
    (RR1 : Prop) (RR2 : Prop) (r : itree E itree E Prop)
    (r0 : ) (t4 : itree E ),
    secure_eqitF Label priv true l id
                 ( (secure_eqit_ Label priv true l id) ) (observe )
                 (RetF )
     t : itree E ,
       (secure_eqit_ Label priv true l id) t
      secure_eqitF Label priv (rcompose ) true l id
                   ( (secure_eqit_ Label priv (rcompose ) true l id) r)
                   (observe t) (RetF ).
Proof.
  intros E Label priv l r t H.
  punfold H. red in H.
  remember (RetF ) as x.
  hinduction before r; intros; inv Heqx; try inv CHECK; auto.
  - remember (RetF ) as y.
    hinduction before r; intros; inv Heqy; eauto with itree.
    rewrite itree_eta'. unpriv_ind. cbn. eapply ; eauto.
  - eapply ; eauto.
    remember (TauF ) as y.
    hinduction H before r; intros; inv Heqy; try inv CHECK; eauto with itree.
    + pclearbot. constructor; auto. pstep_reverse.
    + pclearbot. unpriv_ind. pstep_reverse.
    + pclearbot. punfold H.
  - assert (Hne : nonempty A). { eauto. } (* add the condition that lets us assume this*)
    inv Hne. eapply ( a); eauto.
    remember (VisF e ) as y.
    hinduction before r; intros; inv Heqy; try inv CHECK; ddestruction; subst;
    try contradiction; try contra_size; eauto with itree.
    + pclearbot. constructor; auto. pstep_reverse.
    + pclearbot. unpriv_ind. pstep_reverse.
    + pclearbot. rewrite itree_eta' at 1. pstep_reverse.
Qed.


Lemma eqit_secure_trans_aux2:
   (E : Type Type) (R3 R1 : Type) (Label : Preorder)
    (priv : x : Type, E x L) (l : L) (b2 : bool) (R2 : Type)
    (RR1 : Prop) (RR2 : Prop) (r : itree E itree E Prop)
    (X : Type) (e0 : E X) (k : X itree E ) (t4 : itree E ),
    leq (priv X ) l
    secure_eqitF Label priv true l id
                 ( (secure_eqit_ Label priv true l id) ) (observe )
                 (VisF k)
    ( (t1 : itree E ) (t2 : itree E ) (t3 : itree E ),
        eqit_secure Label priv true l
        eqit_secure Label priv true l r )
     t : itree E ,
       (secure_eqit_ Label priv true l id) t
      secure_eqitF Label priv (rcompose ) true l id
                   ( (secure_eqit_ Label priv (rcompose ) true l id) r)
                   (observe t) (VisF k).
Proof.
  intros E Label priv l r X k t Ht.
  punfold Ht. red in Ht. remember (VisF k) as x.
  hinduction before r; intros; inv Heqx; try inv CHECK;
  ddestruction; subst; try contradiction; eauto.
  - eapply ; eauto. clear . remember (TauF ) as y.
    hinduction Ht before r; intros; inv Heqy; try inv CHECK; eauto with itree.
    + pclearbot. constructor; auto. pstep_reverse.
    + pclearbot. unpriv_ind. pstep_reverse.
    + pclearbot. punfold H.
  - pclearbot. remember (VisF ) as y.
    hinduction Ht before r; intros; inv Heqy; try inv CHECK;
    ddestruction; subst; try contradiction; eauto with itree.
    + pclearbot. constructor; auto. right. eapply . apply H.
      apply .
    + rewrite itree_eta'. unpriv_ind. eapply ; eauto.
  - assert (nonempty A); eauto. inv . eapply ; eauto.
    Unshelve. all : auto. clear . rewrite in H.
    remember (VisF e ) as y.
    hinduction Ht before r; intros; inv Heqy; try inv CHECK; ddestruction; subst;
    try contradiction; try contra_size; eauto with itree.
    + pclearbot. constructor; auto. pstep_reverse.
    + pclearbot. unpriv_ind. pstep_reverse.
    + pclearbot. rewrite itree_eta' at 1. pstep_reverse.

Qed.


Lemma secret_halt_trans_1 : E Label priv l b1 b2 (R1 R2 R3 A : Type) (RR1 : Prop)
            (RR2 : Prop) t1 (e : E A) k t3,
    (¬ leq (priv A e) l )
    empty A
    eqit_secure Label priv l (Vis e k)
    eqit_secure Label priv l (Vis e k)
    eqit_secure Label priv (rcompose ) l .
Proof.
  intros E Label priv l A e k He HA.
  generalize dependent . generalize dependent .
  pcofix CIH. intros .
  pfold. red. punfold . red in . punfold . red in .
  cbn in ×.
  remember (VisF e k) as x.
  hinduction before r; intros; inv Heqx; ddestruction; subst;
  try contradiction; try contra_size; eauto with itree.
  - pclearbot. inv ; ddestruction; subst; try contradiction; try contra_size.
    + constructor. right. apply CIH; auto. pfold. auto.
    + unpriv_co; auto. right. apply CIH; auto. pfold. rewrite in . apply .
    + pclearbot. constructor. right. apply CIH; auto.
    + pclearbot. destruct (classic_empty B).
      × unpriv_halt. right. apply CIH; auto with itree. pfold.
        red. cbn. unpriv_halt.
      × unpriv_co. right. apply CIH; auto. apply .
    + pclearbot. unpriv_halt. right. apply CIH; auto. pfold.
      red. cbn. unpriv_halt. contra_size.
  - pclearbot. inv ; ddestruction; subst; try contradiction; try contra_size.
    + unpriv_halt. right. apply CIH; auto.
      × pfold. red. cbn. unpriv_halt.
      × pfold. auto.
    + unpriv_halt. right. apply CIH; auto.
      × pfold. red. cbn. unpriv_halt.
      × pfold. auto. rewrite in . apply .
    + pclearbot. unpriv_halt. right. apply CIH; auto.
      pfold. red. cbn. unpriv_halt.
    + pclearbot. unpriv_halt. right. apply CIH.
      × pfold. red. cbn. unpriv_halt.
      × apply .
    + unpriv_halt. contra_size.
  - pclearbot. inv ; ddestruction; subst; try contradiction; try contra_size;
    destruct (classic_empty ).
    + unpriv_halt. right. apply CIH; auto.
      × pfold. red. cbn. unpriv_halt. contra_size.
      × pfold. auto.
    + unpriv_co. right. apply CIH; auto; try apply H.
      pfold. auto.
    + unpriv_halt. right. apply CIH; auto.
      × pfold. red. cbn. unpriv_halt. contra_size.
      × pfold. rewrite in . apply .
    + unpriv_co. right. apply CIH. apply H. rewrite in .
      pfold. apply .
    + pclearbot. unpriv_halt. right. apply CIH; auto. pfold.
      red. cbn. unpriv_halt. contra_size.
    + pclearbot. unpriv_co. right. apply CIH; auto. apply H.
    + unpriv_halt. pclearbot. right. apply CIH; try apply .
      pfold. red. cbn. unpriv_halt. contra_size.
    + pclearbot. destruct (classic_empty B).
      × unpriv_halt. right. apply CIH; auto. apply H.
        pfold. red. cbn. unpriv_halt.
      × unpriv_co. right. apply CIH; eauto. apply H. apply .
    + pclearbot. unpriv_halt. contra_size.
    + pclearbot. unpriv_halt. right. apply CIH; auto. apply H.
      pfold. red. cbn. unpriv_halt. contra_size.
Qed.


Lemma secret_halt_trans_2 : E Label priv l b1 b2 (R1 R2 R3 A : Type) (RR1 : Prop)
            (RR2 : Prop) (e : E A) k t2 t3,
    (¬ leq (priv A e) l )
    empty A
    eqit_secure Label priv l (Vis e k)
    eqit_secure Label priv l
    eqit_secure Label priv (rcompose ) l (Vis e k) .
Proof.
  intros E Label priv l A e k He HA.
  generalize dependent . generalize dependent .
  pcofix CIH. intros . pfold.
  red. cbn. punfold . punfold . red in . red in .
  cbn in ×.
  hinduction before r; intros; eauto with itree.
  - inv . ddestruction; subst. contra_size.
  - unpriv_halt. right. pclearbot. eapply CIH; eauto.
    inv ; ddestruction; subst; try contra_size; try contradiction; pclearbot; eauto.
    pfold. auto.
  - eapply ; eauto.
    inv ; ddestruction; subst; try contra_size; try contradiction; pclearbot; eauto.
    punfold .
  - pclearbot.
    inv ; ddestruction; subst; try contra_size; try contradiction; pclearbot; eauto.
  - unpriv_halt. pclearbot. inv SIZECHECK. right. eapply CIH; try apply H.
    Unshelve. all : auto.
    inv ; ddestruction; subst; try contra_size; try contradiction; pclearbot; eauto.
    + pfold. apply .
    + apply .
  - pclearbot. unpriv_halt. right. eapply CIH; try apply H.
    inv ; ddestruction; subst; try contra_size; try contradiction; pclearbot; eauto.
    pfold. auto.
  - pclearbot. unpriv_halt. inv . inv . right. eapply CIH; try apply H.
    Unshelve. all : auto.
    inv ; ddestruction; subst; try contra_size; try contradiction; pclearbot; eauto.
    + pfold. apply .
    + apply .
  - inv SIZECHECK. eapply ; eauto. Unshelve. all : auto.
    inv ; ddestruction; subst; try contra_size; try contradiction; pclearbot; eauto.
    rewrite itree_eta' at 1. pstep_reverse.
  - unpriv_halt. right. eapply CIH; eauto. pfold. apply .
    pfold. apply H.
  - pclearbot. unpriv_halt. right. eapply CIH; eauto. pfold. auto.
  - unpriv_halt. contra_size.
  - unpriv_halt. right. pclearbot. eapply CIH with ( := Vis ); eauto.
    + pfold. auto.
    + apply H.
  - unpriv_halt. contra_size.
Qed.


Lemma eqit_secure_RR_imp : E b1 b2 R1 R2 (RR1 RR2 : Prop) Label priv l
                (t1 : itree E ) (t2 : itree E ),
     <2=
    eqit_secure Label priv l
    eqit_secure Label priv l .
Proof.
  intros. generalize dependent . revert .
  pcofix CIH. intros . pfold. red.
  punfold . red in .
  hinduction before r; intros; eauto;
  try (pclearbot; constructor; auto; right; eapply CIH; eauto; fail);
  try (pclearbot; unpriv_co; right; eapply CIH; eauto; apply ; fail).
  pclearbot. constructor; auto. right. eapply CIH; eauto. apply .
  - pclearbot. unpriv_halt. right. eapply CIH; eauto. apply .
  - pclearbot. unpriv_halt. right. eapply CIH; eauto. apply .
Qed.


Lemma secret_halt_trans_3 : E Label priv l b1 b2 (R1 R2 R3 A : Type) (RR1 : Prop)
            (RR2 : Prop) t1 t2 (e : E A) k,
    (¬ leq (priv A e) l )
    empty A
    eqit_secure Label priv l
    eqit_secure Label priv l (Vis e k)
    eqit_secure Label priv (rcompose ) l (Vis e k).
Proof.
  intros. apply eqit_secure_sym in . apply eqit_secure_sym in .
  apply eqit_secure_sym. eapply secret_halt_trans_2 in ; eauto.
  eapply eqit_secure_RR_imp; eauto.
  intros. inv PR. econstructor; eauto.
Qed.


Lemma eqit_secure_trans : E Label priv l b1 b2 (R1 R2 R3 : Type) (RR1 : Prop)
            (RR2 : Prop) (t1 : itree E ) (t2 : itree E ) (t3 : itree E ),
    eqit_secure Label priv l
    eqit_secure Label priv l
    eqit_secure Label priv (rcompose ) l .
Proof.
  intros E Label priv l .
  pcofix . intros .
  punfold . red in . punfold . red in . pfold. red.
  hinduction before r; intros; try inv CHECK; auto with itree.
  - remember (RetF ) as x.
    hinduction before r; intros; inv Heqx; try inv CHECK; eauto with itree.
    rewrite itree_eta' at 1. unpriv_ind. eapply ; eauto.
  - pclearbot. genobs .
    assert ( ( t5, = TauF ) ( t5, TauF ) ).
    { destruct ; eauto; right; intros; discriminate. }
    destruct as [ [ ] | ].
    + subst. rewrite . rewrite in . constructor.
      right. eapply ; eauto. eapply eqit_secure_TauLR. pfold.
      auto.
    + destruct ; try (exfalso; eapply ; eauto; fail ).
      × inv . inv CHECK. rewrite itree_eta' at 1.
        assert (eqit_secure Label priv (rcompose ) true l (Tau ) (Ret ) ).
        { pfold. red. cbn. rewrite itree_eta' at 1. eapply eqit_secure_trans_aux1; eauto.
          pfold. red. constructor; auto. pstep_reverse. }
        rewrite itree_eta'. pstep_reverse. eapply paco2_mon; eauto.
        intros; contradiction.
      × destruct (classic (leq (priv _ e) l ) ).
        -- inv ; ddestruction; subst; try contradiction; try inv CHECK.
           constructor; auto. eapply eqit_secure_trans_aux2; eauto.
        -- destruct (classic_empty X).
           ++ rewrite itree_eta'. rewrite itree_eta' at 1.
              pstep_reverse.
              eapply paco2_mon with (r := ); intros; try contradiction.
              eapply secret_halt_trans_3 with ( := Tau ); eauto.
              ** pfold. constructor. left. auto.
              ** pfold. auto.
           ++ unpriv_co. right. eapply ; eauto.
              assert (eqit_secure Label priv l (Tau ) (Vis e k)).
              pfold. auto. eapply eqit_secure_TauLVisR; eauto.
  - apply ; auto.
    remember (TauF ) as y.
    hinduction before r; intros; inv Heqy; try inv CHECK; eauto with itree.
    + pclearbot. constructor; auto. pstep_reverse.
    + pclearbot. unpriv_ind. pstep_reverse.
    + pclearbot. punfold H.
  - pclearbot. remember (VisF e ) as x.
    hinduction before r; intros; inv Heqx; try inv CHECK; ddestruction; subst;
    try contradiction; eauto with itree.
    + pclearbot. constructor; auto. intros. right. eapply ; eauto; try apply .
      apply H.
    + rewrite itree_eta' at 1. unpriv_ind. eapply ; eauto.
  - pclearbot. remember (TauF ) as x.
    hinduction before r; intros; inv Heqx; try inv CHECK; auto.
    + pclearbot. unpriv_co. right. eapply ; try apply .
      auto.
    + destruct .
      × clear . rewrite itree_eta'. unpriv_ind.
        remember ( a) as t. specialize (H a). setoid_rewrite Heqt in H.
        clear Heqt a . cbn. eapply eqit_secure_trans_aux1; eauto.
      × unpriv_co. right. eapply ; try apply H.
        clear . remember (TauF t) as y.
        pfold. red.
        hinduction before r; intros; inv Heqy; try inv CHECK; eauto with itree.
        -- pclearbot. constructor; auto. pstep_reverse.
        -- pclearbot. unpriv_ind. pstep_reverse.
        -- pclearbot. punfold H.
      × destruct (classic (leq (priv _ ) l ) ).
        -- rewrite itree_eta'. unpriv_ind. cbn.
           clear . remember ( a) as t. specialize (H a). setoid_rewrite Heqt in H.
           clear Heqt a . eapply eqit_secure_trans_aux2; eauto.
        -- destruct (classic_empty X).
           ++ rewrite itree_eta'. unpriv_ind.
              pstep_reverse. apply paco2_mon with (r := ); intros; try contradiction.
              eapply secret_halt_trans_3; eauto. apply H.
              pfold. auto.
           ++ unpriv_co. right. eapply . apply H.
              clear . pstep. red. remember (VisF k) as y.
              hinduction before r; intros; inv Heqy; try inv CHECK;
                ddestruction; subst; try contradiction; try contra_size; eauto with itree.
              ** pclearbot. constructor; auto. pstep_reverse.
              ** unpriv_ind. pclearbot. pstep_reverse.
              ** pclearbot. rewrite itree_eta' at 1. pstep_reverse.
    + constructor; auto. eapply ; eauto.
    + pclearbot. unpriv_co. right. eapply ; try apply . apply H.
    + rewrite itree_eta' at 1. unpriv_ind. eapply ; eauto.
    + unpriv_halt. right. pclearbot. eapply ; eauto. apply .
  - pclearbot.
    genobs_clear .
    assert (Hne : nonempty A); eauto. inv Hne.
    assert ( ( t4, = TauF ) ( t4, TauF ) ).
    { destruct ; eauto; right; intros; discriminate. }
    destruct as [ [ ] | ].
    + subst. constructor. right. eapply ; try apply H.
      Unshelve. all: auto.
      eapply eqit_secure_TauRVisL; eauto. pfold. auto.
       (* should be fine but new lemma, also shelved goal *)
    +
      destruct ; try (exfalso; eapply ; eauto; fail ).
      × inv ; inv CHECK. ddestruction. subst. clear .
        constructor; auto. rewrite . eapply eqit_secure_trans_aux1; eauto.
        rewrite . apply . Unshelve. auto. (* shelved goal*)
      × constructor. right. eapply ; try apply H.
        eapply eqit_secure_TauRVisL; eauto. pfold. auto.
        (* same goal as last admit *)
      × destruct (classic (leq (priv _ ) l ) ).
        -- inv ; try inv CHECK; ddestruction; subst; try contradiction.
           constructor; auto. rewrite . eapply eqit_secure_trans_aux2; eauto.
           rewrite . apply . Unshelve. all : auto.
        -- destruct (classic_empty X).
           ++ rewrite itree_eta'. rewrite itree_eta' at 1. pstep_reverse.
              eapply paco2_mon with (r := ); intros; try contradiction.
              eapply secret_halt_trans_3 with ( := Vis e ); eauto.
              ** pfold. red. cbn. unpriv_co.
              ** pfold. auto.
           ++ unpriv_co. right. eapply ; try apply H.
              Unshelve. all : auto.
              assert (eqit_secure Label priv l (Vis e ) (Vis k) ).
              pfold. auto. eapply eqit_secure_VisLR; eauto.
  - pclearbot. remember (VisF ) as x.
    (* maybe need to separate the inductive and coinductive progress cases? *)
    hinduction before r; intros; inv Heqx; try inv CHECK; try contradiction;
    try contra_size;
    ddestruction; subst; auto.
    + constructor; auto. eapply ; eauto.
    + pclearbot. unpriv_co. right. eapply ; try apply . apply H.
    + pclearbot. assert (Hne : nonempty B); eauto. inv Hne.
      unpriv_co. right. eapply ; eauto; try eapply . apply H.
      Unshelve. auto.
    + pclearbot. assert (Hne : nonempty ); eauto. inv Hne.
      unpriv_co. right. eapply ; try apply . apply H.
      Unshelve. auto.
    + genobs . destruct .
      × assert (Hne : nonempty B); eauto. inv Hne.
        rewrite itree_eta'. unpriv_ind. eapply eqit_secure_trans_aux1; eauto.
        Unshelve. auto.
      × assert (Hne : nonempty B); eauto. inv Hne.
        unpriv_co. right. eapply ; try apply . Unshelve. all : auto.
        clear . specialize (H a). pfold. red. genobs ( a) .
        clear .
        remember (TauF t) as y.
        hinduction H before r; intros; inv Heqy; try inv CHECK; auto.
        -- constructor; auto. pclearbot. pstep_reverse.
        -- constructor; eauto.
        -- pclearbot. unpriv_ind. pstep_reverse.
        -- unpriv_ind. eapply ; eauto.
        -- pclearbot. rewrite itree_eta' at 1. pstep_reverse.
      × inv .
        destruct (classic (leq (priv _ e) l ) ).
        -- rewrite itree_eta'. unpriv_ind.
           eapply eqit_secure_trans_aux2; eauto. Unshelve. all : auto.
        -- destruct (classic_empty X).
           ++ unpriv_halt. right. eapply ; eauto. apply .
              pfold. apply H. Unshelve. auto.
           ++ unpriv_co. right. eapply ; try apply .
              Unshelve. all : auto.
              clear . pstep. red. remember (VisF e k) as y.
              specialize (H a). clear . genobs ( a) .
              clear .
              hinduction H before r; intros; inv Heqy; try inv CHECK;
                ddestruction; subst; try contradiction; try contra_size; eauto with itree.
              ** pclearbot. constructor; auto. pstep_reverse.
              ** unpriv_ind. pclearbot. pstep_reverse.
              ** pclearbot. rewrite itree_eta' at 1. pstep_reverse.
    + rewrite itree_eta' at 1. unpriv_ind. eapply ; eauto.
    + pclearbot. inv . unpriv_halt. right. eapply ; eauto. apply .
      apply H. Unshelve. auto.
  - remember (VisF e ) as x. hinduction before r; intros; inv Heqx; try inv CHECK;
    ddestruction; subst; try contradiction; try contra_size; auto.
    + constructor; auto. eapply ; eauto.
    + constructor; auto. pclearbot. assert (Hne : nonempty ); eauto. inv Hne. eapply ; eauto.
      pstep_reverse. Unshelve. auto.
    + unpriv_ind. assert (Hne : nonempty ); eauto. inv Hne. eapply ; eauto.
      pclearbot. pstep_reverse. Unshelve. auto.
    + assert (Hne : nonempty ). { eauto. } inv Hne. eauto. Unshelve. auto.
    + unpriv_ind. eauto.
    + pclearbot. rewrite itree_eta'. pstep_reverse.
      apply paco2_mon with (r := ); intros; try contradiction.
      inv .
      eapply secret_halt_trans_3 with ( := a); eauto.
      × pfold. apply .
      × apply H.
  - pclearbot.
    remember (TauF ) as y.
    hinduction before r; intros; inv Heqy; subst; eauto with itree; pclearbot.
    + unpriv_halt. right. eapply ; eauto.
    + clear . rewrite itree_eta'. rewrite itree_eta' at 1.
      pstep_reverse. apply paco2_mon with (r := ); intros; try contradiction.
      eapply secret_halt_trans_2; eauto. pfold. auto.
    + unpriv_halt. right. eapply ; eauto. apply H.
    + rewrite itree_eta' at 1. unpriv_ind. eapply ; eauto.
    + unpriv_halt. contra_size.
  - pclearbot.
    inv ; ddestruction; subst; try contra_size; try contradiction;
    try inv CHECK.
    + constructor. right. eapply ; eauto. pfold. auto.
    + unpriv_co. right. eapply ; eauto. rewrite in .
      pfold. apply .
    + pclearbot. constructor. right. eapply ; eauto.
    + pclearbot. destruct (classic_empty B).
      × unpriv_halt. right. eapply ; eauto. pfold. red. cbn. unpriv_halt.
      × unpriv_co. right. eapply ; eauto. apply .
    + pclearbot. unpriv_halt. right. eapply ; eauto.
      pfold. red. cbn. unpriv_halt. contra_size.
 - pclearbot. rewrite itree_eta' at 1. pstep_reverse.
   apply paco2_mon with (r := ); intros; try contradiction.
   eapply secret_halt_trans_2 with ( := Vis ); eauto.
   + pfold. red. cbn. unpriv_halt.
   + pfold. auto.
 - pclearbot. destruct (classic_empty A).
   + inv ; ddestruction; subst; try contradiction; try contra_size; try inv CHECK.
     × unpriv_halt. right. eapply with ( := Vis ); eauto.
       -- pfold. red. cbn. unpriv_halt. contra_size.
       -- pfold. auto.
     × unpriv_halt. right. rewrite in . eapply with ( := Vis ); eauto.
       -- pfold. red. cbn. unpriv_halt. contra_size.
       -- pfold. apply .
     × unpriv_halt. pclearbot. right. eapply ; eauto.
       pfold. red. cbn. unpriv_halt. contra_size.
     × unpriv_halt. pclearbot. right. eapply with ( := Vis ); eauto.
       -- pfold. red. cbn. unpriv_halt. contra_size.
       -- apply .
     × unpriv_halt. contra_size.
   + destruct (observe ).
     × inv ; ddestruction; subst; try contra_size; try contradiction.
     × unpriv_co. right. eapply ; eauto. apply H.
       inv ; ddestruction; subst; try contra_size; try contradiction.
       pfold. auto. pclearbot. auto.
     × destruct (classic (leq (priv _ e) l ) ).
       { inv ; ddestruction; subst; try contra_size; try contradiction. }
       destruct (classic_empty X).
       -- unpriv_halt. right. eapply ; eauto. apply H. pfold. auto.
       -- unpriv_co. right. eapply ; eauto. apply H.
          inv ; ddestruction; subst; try contra_size; try contradiction.
          ++ pfold. apply .
          ++ pclearbot. apply .
Qed.


Lemma eqit_itree_eqit_secure : E Label priv l R1 R2 RR (t1 t1': itree E ) (t2 : itree E ),
     eqit_secure Label priv RR false false l
    eqit_secure Label priv RR false false l .
Proof.
  intros E Label priv l RR. pcofix CIH.
  intros Heq Hsec. pstep. red.
  punfold Heq. red in Heq. punfold Hsec. red in Hsec.
  inv Heq; try inv CHECK.
  - rewrite in Hsec. rewrite itree_eta' at 1. pstep_reverse.
    eapply paco2_mon with (r := ); intros; try contradiction. pfold.
    red. cbn. remember (RetF ) as x. clear H .
    hinduction Hsec before r; intros; inv Heqx; eauto with itree.
  - pclearbot. genobs .
    assert ( ( t3, = TauF ) ( t3, TauF ) ).
    { destruct ; eauto; right; intros; discriminate. }
    destruct as [ [ ] | ].
    + subst. rewrite . rewrite in Hsec. constructor.
      right. eapply CIH; eauto. rewrite in Hsec. inv Hsec; try inv CHECK. pclearbot. auto.
    + destruct ; try (exfalso; eapply ; eauto; fail ).
      × rewrite in Hsec. inv Hsec; try inv CHECK.
      × rewrite in Hsec. inv Hsec; ddestruction; subst; try inv CHECK.
        -- pclearbot. unpriv_co. right. eapply CIH; eauto. apply .
        -- pclearbot. unpriv_halt. right. eapply CIH; eauto.
  - rewrite in Hsec. inv Hsec; ddestruction; subst; try inv CHECK; try contradiction; try contra_size.
    + pclearbot. constructor; auto. right. eapply CIH; eauto with itree. apply .
    + pclearbot. unpriv_co. right. eapply CIH; eauto with itree. apply .
    + pclearbot. unpriv_co. right. eapply CIH; eauto with itree. apply .
    + pclearbot. unpriv_halt. right. eapply CIH; eauto. pfold. constructor. left. auto.
    + pclearbot. unpriv_halt. right. eapply CIH with ( := Vis e ); try apply .
      pfold. constructor. left. auto.
    + pclearbot. unpriv_halt. right. eapply CIH; eauto with itree. apply .
Qed.


Lemma eqit_secure_eq_trans : E R b1 b2 Label priv l (t1 t2 t3 : itree E R),
    eqit_secure Label priv eq l
    eqit_secure Label priv eq l
    eqit_secure Label priv eq l .
Proof.
  intros. apply eqit_secure_RR_imp with ( := rcompose eq eq).
  { intros. inv PR. auto. }
  eapply eqit_secure_trans; eauto.
Qed.


Lemma eqit_secure_anything : E R1 b Label priv l
                      (t1 : itree E ) t2,
    eqit_secure Label priv eq b b l
    eqit_secure Label priv eq b b l .
Proof.
  intros.
  eapply eqit_secure_eq_trans; eauto.
  apply eqit_secure_sym. eapply eqit_secure_RR_imp; eauto.
Qed.


Global Instance proper_eqit_secure_eqit {E} {R1 R2 : Type} {b} {RR : Prop} {Label priv l} :
       Proper (eqit eq b b eqit eq b b iff) (@eqit_secure E Label priv RR b b l).
Proof.
  repeat intro. destruct b; split; intros.
  - eapply eutt_secure_eqit_secure; eauto.
    apply eqit_secure_sym. eapply eutt_secure_eqit_secure; eauto.
    apply eqit_secure_sym. auto.
  - assert (x y); auto. assert ( ); auto.
    symmetry in .
    eapply eutt_secure_eqit_secure; eauto.
    symmetry in . apply eqit_secure_sym.
    eapply eutt_secure_eqit_secure; eauto.
    apply eqit_secure_sym. auto.
  - eapply eqit_itree_eqit_secure; eauto.
    apply eqit_secure_sym. eapply eqit_itree_eqit_secure; eauto.
    apply eqit_secure_sym. auto.
  - assert (x y); auto. assert ( ); auto.
    symmetry in . symmetry in .
    eapply eqit_itree_eqit_secure; eauto.
    apply eqit_secure_sym. eapply eqit_itree_eqit_secure; eauto.
    apply eqit_secure_sym. auto.
Qed.


Global Instance proper_eqit_secure_eqit_secure
       {E} {b} {R1 R2 : Type} {RR : Prop} {Label priv l} :
  Proper (eqit_secure Label priv eq b b l eqit_secure Label priv eq b b l iff)
         (@eqit_secure E Label priv RR b b l).
Proof.
  repeat intro; split; intros.
  - eapply eqit_secure_RR_imp with ( := rcompose RR eq); eauto.
    { intros. inv PR. auto. }
    eapply eqit_secure_trans; eauto.
    apply eqit_secure_sym.
    eapply eqit_secure_RR_imp with ( := rcompose (flip RR) eq); eauto.
    { intros. inv PR. auto. }
    eapply eqit_secure_trans; eauto. apply eqit_secure_sym. auto.
  - assert (eqit_secure Label priv eq b b l ).
    { apply eqit_secure_sym. eapply eqit_secure_RR_imp; eauto. }
    eapply eqit_secure_RR_imp with ( := rcompose RR eq).
    { intros. inv PR. auto. }
    eapply eqit_secure_trans; eauto.
    assert (eqit_secure Label priv eq b b l y x).
    { apply eqit_secure_sym. eapply eqit_secure_RR_imp; eauto. }
    eapply eqit_secure_RR_imp with ( := rcompose eq RR).
    { intros. inv PR. auto. }
    eapply eqit_secure_trans; eauto.
Qed.