proposition: Lemma rtclosure_eq_union_rclosure_tclosure : forall R, rtclosure R = union (rclosure R) (tclosure R).
proof: Proof. Proof using. extens. intros x y. unfold union. iff M. { induction* M. destruct IHM1 as [H1|H1]; destruct IHM2 as [H2|H2]. { destruct H1; destruct* H2. } { destruct* H1. } { destruct* H2. } { autos*. } } { destruct* M. { applys* rtclosure_of_rclosure. } { applys* rtclosure_of_tclosure. } } Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)