proposition: Lemma euttVC_flip gH r: flip (euttVC (flip RR) (flip gH) (flip r)) <2= @euttVC E R1 R2 RR gH r.
proof: Proof. pcofix CIH. intros. gunfold PR. gclo. apply rclo_transD. eapply rclo_flip; eauto with paco. eapply rclo2_mon_gen; eauto; intros. { eapply transD_flip. eauto. } destruct PR0; cycle 1. { gbase. destruct H; eauto using transU_flip with itree. } gstep. apply eqitF_flip. eapply eqitF_mono; eauto with paco. intros. gbase. eapply CIH. eapply gupaco2_mon; eauto. intros. destruct PR1; eauto. Qed.
imports: Coq(Setoid Morphisms Relations) Paco(paco) ITree(Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.Paco2 Eq.Shallow)