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