proposition: Lemma stclosure_eq_rstclosure_of_refl : forall R, refl R -> stclosure R = rstclosure R.
proof: Proof. Proof using. introv H. extens. intros x y. iff M. { applys* rstclosure_of_stclosure. } { induction* M. } Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)