proposition: Lemma infseq_inv': forall a b, R a b -> infseq a -> infseq b.
proof: Proof. intros a b Rab Ia. destruct (infseq_inv Ia) as (b' & Rab' & Xb'). assert (b' = b) by (eapply R_functional; eauto). subst b'. auto. Qed.