proposition: Lemma sutt_inv_vis {E R1 R2} (RR : R1 -> R2 -> Prop) : forall X e (k1 : X -> itree E R1) (k2 : X -> itree E R2), sutt RR (Vis e k1) (Vis e k2) -> forall x, sutt RR (k1 x) (k2 x).
proof: Proof. intros. pstep. punfold H. simpl in *. eapply suttF_inv_vis in H; pclearbot; punfold H. Qed.
imports: Paco(paco) Coq(Morphisms) ITree(Axioms Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.UpToTaus Eq.Shallow Eq.Paco2)