Theorem isdeceqbool: isdeceq bool. 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.