proposition: Lemma adjacent_unique2 A (r: relation A) (ACYC: acyclic r): forall a b c : A, r b a -> r c a -> adjacent r b a -> adjacent r c a -> b = c.
proof: Proof. ins; unfold adjacent in *; desc. assert (r^? b c) by eauto. assert (r^? c b) by eauto. unfolder in *; desf. by exfalso; eapply ACYC; eapply t_trans; econs; eauto. Qed.
imports: HahnBase HahnRelationsBasic HahnRewrite Setoid