proposition: Lemma equiv_join R x y z: star R x z -> star R y z -> equiv R x y.
proof: Proof. intros. transitivity z. rewrite H; reflexivity. symmetry. rewrite H0; reflexivity. Qed.
imports: Morphisms FinFun Undecidability.HOU(std.tactics)