proposition: Lemma fold_ruttF: forall (t1: itree E1 R1) (t2: itree E2 R2) ot1 ot2, ruttF (upaco2 rutt_ bot2) ot1 ot2 -> ot1 = observe t1 -> ot2 = observe t2 -> rutt t1 t2.
proof: Proof. intros * eq -> ->; pfold; auto. Qed.
imports: Coq(Morphisms ) ExtLib(Structures.Monad) ITree(Basics.Utils Axioms ITree Eq Basics ) Paco(paco)