proposition: Lemma equiv_reduce R x x' y y' : star R x x' -> star R y y' -> equiv R x y -> equiv R x' y'.
proof: Proof. intros. eapply equiv_trans. eapply equiv_symm, equiv_star, H. now eapply equiv_trans, equiv_star, H0. Qed.
imports: Morphisms FinFun Undecidability.HOU(std.tactics)