proposition: Lemma eutt_disj_l {E} {R S} {RS RS'} : forall (t : itree E R) (s : itree E S), eutt RS t s -> eutt (RS \2/ RS') t s.
proof: Proof. intros. eapply eqit_mon with (RR := RS); eauto. Qed.
imports: Coq(Setoid Morphisms Relations) Paco(paco) ITree(Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.Paco2 Eq.Shallow)