proposition: Lemma euttVC_gen gH r: transU RR (gupaco2 (eqit_ RR true true (euttVC RR gH)) (transD RR) (transU RR (r \2/ gH))) <2= @euttVC E R1 R2 RR gH r.
proof: Proof. intros. eapply euttG_transU_aux in PR; eauto using transU_compose. revert x0 x1 PR. pcofix CIH. intros. gunfold PR. apply rclo_transD in PR. gclo. eapply transD_mon; eauto. intros. destruct PR0; eauto with paco. gstep. red in H |- *. induction H; auto with itree. - econstructor. gbase. eapply CIH. eapply gupaco2_mon; eauto. intros. destruct PR0; eauto. - econstructor. intros. gbase. eapply CIH. red in REL. gupaco. eapply gupaco2_mon_gen; eauto with paco; intros. + eapply eqitF_mono; eauto with paco. + eapply euttG_transU_aux; eauto using transU_compose with paco. eapply transU_mon; eauto. intros. destruct PR1; [|eauto 7 with paco]. 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)