proposition: Lemma euttG_cofix_aux: forall rH rL gL gH x, (x <2= euttG rH rL (gL \2/ x) (gH \2/ x)) -> (x <2= euttG rH rL gL gH).
proof: Proof. intros. apply euttG_gen. econstructor. revert x0 x1 PR. pcofix CIH. intros t1 t2 PR. apply H in PR. destruct PR as [IN]. revert t1 t2 IN. pcofix CIH. intros. apply gpaco2_dist in IN; eauto with paco. destruct IN; cycle 1. { apply rclo_transD in H0; eauto with paco. gclo. eapply transD_mon; eauto with paco. } assert (LEM: upaco2 (eqit_ RR true true (euttVC RR (gH \2/ x))) (rclo2 (transD RR) ((gL \2/ x) \2/ (transU RR rH \2/ rL))) <2= gpaco2 (eqit_ RR true true (euttVC RR gH)) (transD RR) r0 r0). { intros m1 m2 [REL|REL]. - gbase. apply CIH1. gpaco. gfinal. right. eapply paco2_mon; eauto. intros. apply rclo_transD in PR. gclo. eapply transD_mon; eauto. intros. gbase. repeat destruct PR0 as [PR0|PR0]; eauto. - apply rclo_transD in REL. gclo. eapply transD_mon; eauto. intros. gbase. repeat destruct PR as [PR|PR]; eauto. } punfold H0. gstep. red in H0 |- *. induction H0; auto 3 with itree. red in REL. econstructor. intros. eapply gupaco2_mon; eauto. intros. apply transU_dist in PR. destruct PR; eauto using transU_mon. eapply transU_mon; eauto. intros; destruct PR; eauto with paco. Qed.
imports: Coq(Setoid Morphisms Relations) Paco(paco) ITree(Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.Paco2 Eq.Shallow)