proposition: Lemma infseq_coinduction_principle: forall (X: A -> Prop), (forall a, X a -> exists b, plus a b /\ X b) -> forall a, X a -> infseq a.
proof: Proof. intros X H a0 Xa0. exists (fun a => exists b, star a b /\ X b); split. - exists a0; auto using star_refl. - intros a1 (a2 & S12 & X2). inversion S12; subst. + destruct (H a2 X2) as (a3 & P23 & X3). inversion P23; subst. exists b; split; auto. exists a3; auto. + exists b; split; auto. exists a2; auto. Qed.