left. apply eq_f. assumption.
right.intro.apply H.apply injective_nn.assumption.
right.apply not_eq_nn_cons.
intros.right.intro.apply not_eq_pp_cons m x f1.apply sym_eq.assumption.
intros.right.intro.apply not_eq_nn_cons m x f1.apply sym_eq.assumption.
intros.elim H.
left. apply eq_f. assumption.
right.intro.apply H.apply injective_nn.assumption.
right.apply not_eq_nn_cons.
intros.right.intro.apply not_eq_pp_cons m x f1.apply sym_eq.assumption.
intros.right.intro.apply not_eq_nn_cons m x f1.apply sym_eq.assumption.
intros.elim H.