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