proposition: Lemma rclosure_strict : forall R, refl R -> rclosure (strict R) = R.
proof: Proof. Proof using. Hint Constructors rclosure. unfold strict. extens. intros x y. iff K. { destruct K; subst*. } { tests: (x = y); subst*. } Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)