proposition: Lemma suttF_inv_tau_left {E R1 R2} (RR : R1 -> R2 -> Prop) : forall (t1: itree E R1) ot2, suttF RR (upaco2 (suttF RR) bot2) (TauF t1) ot2 -> suttF RR (upaco2 (suttF RR) bot2) (observe t1) ot2.
proof: Proof. intros. remember (TauF t1) as ott1. induction H; intros; subst; try dependent destruction Heqott1; eauto with itree. pclearbot. punfold EQTAUS. Qed.
imports: Paco(paco) Coq(Morphisms) ITree(Axioms Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.UpToTaus Eq.Shallow Eq.Paco2)