Lemma logeq_dec {X Y} : (X <-> Y) -> decidable X -> decidable Y. Proof. intros iff decX. induction iff as [XtoY YtoX]. induction decX as [x|nx]. - now apply ii1, XtoY. - now apply ii2, (negf YtoX). Defined.
Require Import UniMath.MoreFoundations.Tactics.