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