proposition: Lemma refl_trans_clos_is_trans : forall A (R : relation A) a b c, refl_trans_clos R a b -> refl_trans_clos R b c -> refl_trans_clos R a c.
proof: Proof. intros A R a b c [a' | a' b' Hab]; subst; trivial. intro Hbc; revert Hbc Hab; intros [b'' | b'' c' Hbc] Hab; subst; trivial. apply t_clos; assumption. apply t_clos; apply trans_clos_is_trans with b''; assumption. Qed.
imports: Coq(Setoid Relations List Utf8)