Require Import Streams. Require Import CpdtTactics. Set Implicit Arguments. Print Acc. Print well_founded. Print Stream. CoInductive infiniteDecreasingChain A (R : A -> A -> Prop) : Stream A -> Prop := | ChainCons : forall x y s, infiniteDecreasingChain R (Cons y s) -> R y x -> infiniteDecreasingChain R (Cons x (Cons y s)). Lemma noBadChains' : forall A (R : A -> A -> Prop) x, Acc R x -> forall s, ~infiniteDecreasingChain R (Cons x s). induction 1; crush. match goal with | [ H : infiniteDecreasingChain _ _ |- _ ] => inversion H; eauto end. Qed. Theorem noBadChains : forall A (R : A -> A -> Prop), well_founded R -> forall s, ~infiniteDecreasingChain R s. destruct s; apply noBadChains'; auto. Qed.