proposition: Lemma eutt_sub_self {E R} (R1 R2: R -> R -> Prop) (t: itree E R): (forall r, R1 r r -> R2 r r) -> eutt R1 t t -> eutt R2 t t.
proof: Proof. intros Hrel; revert t. ginit. gcofix CIH; intros t Heutt. punfold Heutt; red in Heutt. remember t as t' in Heutt at 2. assert (Ht': t' ≈ t) by now subst. clear Heqt'. rewrite (itree_eta t). rewrite (itree_eta t), (itree_eta t') in Ht'. revert Ht'. induction Heutt; clear t; intros Heq. - apply eutt_inv_Ret in Heq; subst. gstep; constructor; auto. - apply eqit_inv_Tau in Heq. gstep; constructor. gfinal; left. eapply CIH. rewrite <- Heq at 2. now pclearbot. - gstep; constructor. intros v. eapply eqit_inv_Vis in Heq. gfinal; left. apply CIH. specialize (REL v). rewrite <- Heq at 2. now pclearbot. - rewrite tau_euttge, (itree_eta t1). apply IHHeutt. rewrite tau_euttge in Heq. rewrite <- itree_eta; auto. - apply IHHeutt. rewrite tau_euttge in Heq. rewrite <- itree_eta; auto. Qed.
imports: Coq(Setoid Morphisms Relations) Paco(paco) ITree(Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.Paco2 Eq.Shallow)