Section Accesible_and_Infinte.

Variable A : Set.
Variable R : A → A → Prop.

CoInductive Inf : A → Prop :=
    inf : ∀ x y : A, R y x → Inf y → Inf x.

Theorem NotBoth : ∀ x : A, Acc R x → Inf x → False.
fix 2.
intros x H.
case H.
intros.
inversion_clear H1.
apply (NotBoth y).
apply (H0 y).
assumption.
assumption.
Qed.

End Accesible_and_Infinte.