proposition: Lemma antisym_rclosure : forall R, antisym R -> antisym (rclosure R).
proof: Proof. Proof using. unfolds antisym. introv M N1 N2. destruct N1; destruct N2; subst*. Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)