proposition: Lemma euttG_le_eutt: euttG bot2 bot2 bot2 bot2 <2= eutt RR.
proof: Proof. intros. destruct PR. assert(paco2 (eqit_ RR true true (euttVC RR bot2)) bot2 x0 x1). { eapply gpaco2_init; eauto with paco. eapply gpaco2_mon; eauto; intros; repeat destruct PR as [PR|PR]; destruct PR; contradiction. } clear IN. revert x0 x1 H. pcofix CIH. intros. punfold H. pstep. unfold_eqit. induction H; pclearbot; auto with itree. econstructor; intros. specialize (REL v). right. apply CIH. ginit. gupaco. eapply gupaco2_mon_gen; eauto with paco; intros. - eapply eqitF_mono; eauto with paco. - apply euttG_transU_aux. { intros. destruct PR0; contradiction. } eapply transU_mon; eauto. intros. pclearbot. gfinal. eauto. Qed.
imports: Coq(Setoid Morphisms Relations) Paco(paco) ITree(Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.Paco2 Eq.Shallow)