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