proposition: Lemma rtclosure_inv_rclosure_or_tclosure : forall R x y, rtclosure R x y -> x = y \/ tclosure R x y.
proof: Proof. Proof using. introv M. rewrite rtclosure_eq_union_rclosure_tclosure in M. destruct M as [M|M]. { destruct* M. } { auto. } Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)