proposition: Lemma all_infinite_euttNoRet : forall (E : Type -> Type) (A B : Type) (R : A -> B -> Prop) (ta : itree E A) (tb : itree E B), all_infinite ta -> eutt R ta tb -> euttNoRet ta tb.
proof: Proof. intros E A B R. pcofix CIH. pstep. intros ta tb Hdiv Heutt. punfold Heutt. unfold_eqit. dependent induction Heutt; pclearbot. - exfalso. clear CIH. specialize (itree_eta ta) as Hta. rewrite <- x0 in Hta. rewrite Hta in Hdiv. pinversion Hdiv. - rewrite <- x0. rewrite <- x. constructor. right. assert (m1 ≈ ta). { specialize (itree_eta ta) as Hta. rewrite <- x0 in Hta. rewrite Hta. rewrite tau_eutt. reflexivity. } assert (m2 ≈ tb). { specialize (itree_eta tb) as Htb. rewrite <- x in Htb. rewrite Htb. rewrite tau_eutt. reflexivity. } apply CIH; auto. rewrite H. auto. - rewrite <- x0. rewrite <- x. constructor. intros. right. apply CIH; auto with itree. specialize (itree_eta ta) as Hta. rewrite <- x0 in Hta. rewrite Hta in Hdiv. pinversion Hdiv. dependent destruction H2. apply H0. - rewrite <- x. constructor; auto. eapply IHHeutt; eauto. assert (t1 ≈ ta). { specialize (itree_eta ta) as Hta. rewrite <- x in Hta. rewrite Hta. rewrite tau_eutt. reflexivity. } rewrite H. auto. - rewrite <- x. constructor; auto. Qed.
imports: Coq(Morphisms ) ITree(Axioms ITree ITreeFacts Props.Infinite ) Paco(paco)