Definition isdecrel_natneq : isdecrel (λ m n, m ≠ n). Proof. intros n. induction n as [|n N]. - intro m. induction m as [|m _]. + simpl. exact (ii2 (idfun ∅)). + simpl. exact (ii1 tt). - intro m. induction m as [|m _]. + simpl. exact (ii1 tt). + exact (N m). Defined.