proposition: Lemma finseq_unique: forall a b b', star a b -> irred b -> star a b' -> irred b' -> b = b'.
proof: Proof. intros. destruct (star_star_inv H H1). - inversion H3; subst. auto. elim (H0 _ H4). - inversion H3; subst. auto. elim (H2 _ H4). Qed.