proposition: Lemma antisym_wrt_inverse : forall E R, antisym_wrt E R -> antisym_wrt E (inverse R).
proof: Proof. Proof using. intros_all. unfolds inverse. auto. Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)