proposition: Lemma reflexive_suttF `{Reflexive _ RR} sutt (r1:Reflexive sutt) : Reflexive (@suttF E _ _ RR sutt).
proof: Proof. unfold Reflexive. intros x. destruct x; eauto with itree. Qed.
imports: Paco(paco) Coq(Morphisms) ITree(Axioms Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.UpToTaus Eq.Shallow Eq.Paco2)