proposition: Lemma equiv_symm R x y: equiv R x y -> equiv R y x.
proof: Proof. induction 1. constructor; eauto. eapply star_trans; eauto. econstructor 2; eauto using refl_equiv, sym_symmetric. Qed.
imports: Morphisms FinFun Undecidability.HOU(std.tactics)