left.apply eq_f. assumption.
right.intro.apply H.apply injective_pp.assumption.
right.apply not_eq_pp_nn.
right.apply not_eq_pp_cons.
intros. elim g1.
left.apply eq_f. assumption.
right.intro.apply H.apply injective_pp.assumption.
right.apply not_eq_pp_nn.
right.apply not_eq_pp_cons.
intros. elim g1.