proposition: Lemma suttF_inv_vis {E R1 R2} (RR : R1 -> R2 -> Prop) sutt : forall X e (k1 : X -> itree E R1) (k2 : X -> itree E R2), suttF RR sutt (VisF e k1) (VisF e k2) -> forall x, sutt (observe (k1 x)) (observe (k2 x)).
proof: Proof. intros. inv H. ddestruction; auto. Qed.
imports: Paco(paco) Coq(Morphisms) ITree(Axioms Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.UpToTaus Eq.Shallow Eq.Paco2)