proposition: Lemma sutt_inv_tau_left {E R1 R2} (RR : R1 -> R2 -> Prop) : forall (t1: itree E R1) (t2: itree E R2), sutt RR (Tau t1) t2 -> sutt RR t1 t2.
proof: Proof. intros. punfold H. pstep. repeat red in H |- *. apply suttF_inv_tau_left; auto. Qed.
imports: Paco(paco) Coq(Morphisms) ITree(Axioms Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.UpToTaus Eq.Shallow Eq.Paco2)