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