proposition: Lemma star_star_inv: forall a b, star a b -> forall c, star a c -> star b c \/ star c b.
proof: Proof. induction 1; intros. - auto. - inversion H1; subst. + right. eauto using star. + assert (b = b0) by (eapply R_functional; eauto). subst b0. apply IHstar; auto. Qed.