proposition: Lemma rclosure_eq_of_refl : forall R, refl R -> rclosure R = R.
proof: Proof. Proof using. unfolds refl. introv H. extens. iff M. { destruct M; subst*. } { auto. } Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)