proposition: Lemma rsclosure_eq_union_rclosure_sclosure : forall R, rsclosure R = union (rclosure R) (sclosure R).
proof: Proof. Proof using. extens. intros x y. unfold union. iff M. { induction* M. destruct* IHM as [H|H]. destruct* H. } { destruct* M as [H|H]. destruct* H. applys* rsclosure_of_sclosure. } Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)