proposition: Lemma trans_clos_trans_clos_alt : forall A (R : relation A) x y, trans_clos R x y <-> trans_clos_alt R x y.
proof: Proof. intros A R; split; intro H; induction H. left; assumption. apply trans_clos_alt_is_trans with y; trivial. left; assumption. left; assumption. apply trans_clos_is_trans with y; trivial. left; assumption. Qed.
imports: Coq(Setoid Relations List Utf8)