proposition: Lemma eutt_Vis_spin_abs: forall {E R1 R2} {RR: R1 -> R2 -> Prop} {X} (e: E X) (k: X -> itree E R1), eutt RR (Vis e k) (@ITree.spin E R2) -> False.
proof: Proof. intros. punfold H. unfold eqit_ in H. remember (observe (Vis e k)) as x. remember (observe (ITree.spin)) as sp. revert Heqx Heqsp. induction H; intros EQ1 EQ2; try (now inv EQ1 || now inv EQ2). - apply IHeqitF; auto. inv EQ2. reflexivity. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)