proposition: Lemma monotone_suttF : monotone2 (@suttF E _ _ RR).
proof: Proof. repeat red; intros. induction IN; eauto with itree. Qed.
imports: Paco(paco) Coq(Morphisms) ITree(Axioms Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.UpToTaus Eq.Shallow Eq.Paco2)