proposition: Theorem isdeceqbool: isdeceq bool.
proof: Proof. unfold isdeceq. intros x' x. induction x. - induction x'. + apply (ii1 (idpath true)). + apply (ii2 nopathsfalsetotrue). - induction x'. + apply (ii2 nopathstruetofalse). + apply (ii1 (idpath false)). Defined.
imports: UniMath.Foundations.PartA