proposition: Lemma inverse_equiv : forall A (E:binary A), equiv E -> equiv (inverse E).
proof: Proof. Proof using. introv Equi. unfold inverse. constructor; intros_all; dintuition eauto. Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)