elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False)).
left. apply eq_f. assumption.
right.intro.apply H.apply injective_nn.assumption.
right.apply not_eq_nn_cons.
elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False)).
left. apply eq_f. assumption.
right.intro.apply H.apply injective_nn.assumption.
right.apply not_eq_nn_cons.