proposition: Lemma strict_rclosure : forall R, irrefl R -> strict (rclosure R) = R.
proof: Proof. Proof using. unfold strict. extens. intros x y. iff (K1&K2) K. { destruct* K1. } { split. { left*. } { apply* irrefl_inv_neq. } } Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)