proposition: Lemma euttG_flip gH r: flip (gupaco2 (eqit_ (flip RR) true true (euttVC (flip RR) (flip gH))) (transD (flip RR)) (flip r)) <2= gupaco2 (@eqit_ E R1 R2 RR true true (euttVC RR gH)) (transD RR) r.
proof: Proof. pcofix CIH; intros. destruct PR. econstructor. eapply rclo_flip; eauto with paco. eapply rclo2_mon_gen; [ eauto using transD_flip with itree .. | ]. intros. destruct PR; [ | eauto with itree ]. left. punfold H. pstep. apply eqitF_flip. eapply eqitF_mono; eauto with paco; intros. - eapply euttVC_flip. apply PR. - apply rclo_flip; eauto with paco. eapply rclo2_mon_gen; [ eauto using transD_flip with paco itree .. | ]. intros. right. left. destruct PR0. + eapply CIH. red. eauto with paco. + apply CIH0. destruct H0; eauto. Qed.
imports: Coq(Setoid Morphisms Relations) Paco(paco) ITree(Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.Paco2 Eq.Shallow)