proposition: Lemma tclosure_inv_l : forall R x z, tclosure R x z -> (R x z) \/ (exists y, R x y /\ tclosure R y z).
proof: Proof. Proof using. intros R. applys* tclosure_ind_l. Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)