proposition: Lemma total_rstclosure : forall R, total R -> total (rstclosure R).
proof: Proof. Proof using. unfolds total. introv H. intros x y. destruct* (H x y). Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)