proposition: Lemma trans_clos_is_clos : forall A (R : relation A) a b, trans_clos (trans_clos R) a b -> trans_clos R a b.
proof: Proof. intros A R a b Hab; induction Hab as [a b Hab | a b c Hab Hbc]; trivial. apply trans_clos_is_trans with b; trivial. Qed.
imports: Coq(Setoid Relations List Utf8)