proposition: Lemma refl_trans_clos_is_refl_trans_clos : forall A (R : relation A) a b, refl_trans_clos R a b <-> a = b \/ trans_clos R a b.
proof: Proof. intros A R a b; split; intro H. inversion H as [a' | a' b']. left; apply eq_refl. right; assumption. destruct H as [H | H]. subst b; apply r_step. apply t_clos; assumption. Qed.
imports: Coq(Setoid Relations List Utf8)